Abstract I add a new inference rule to formal systems in such a way that we introduce additional statements that can be proved without getting rid of being sure in their trueness, so producing a new logic (earlier when this was yet vaguely formulated, I called it “Not Logic” on my theological site). The idea was conceived in my theological musings.
Keywords first-order predicate logic, formal system, not logic, logical system
Competing Interests none
TODO: A related article
Our purpose
This article demonstrates another system instead of first-order predicate logic where it is possible to demonstrate (“prove”) from axioms more theorems than in first-order predicate logic.
It is done by modeling additional axioms in supposition that “old” axioms are true, so adding new axioms without risk of going into a contradiction. Moreover, I show that order of adding new axioms is irrelevant, thus I produced a new inference rule.
Worth note that it seems plausible that somebody (e.g. in the galaxy) knows an efficient NP-complete algorithm, but does not know these new inference rules. I deem probable that these new inference rules may shorten complex proofs super-exceptionally and so asymptotically be more powerful knowledge that an efficient NP-complete algorithm.
Remark Below adding axioms that cannot be proved makes sense because of Godel’s incompleteness theorem.
Formal consideration
We will do our considerations in ZF to easily model sets of symbols. (It seems to be generalizable to PA by analogy with Godel’s works.)
Let S = (L,Z) be an axiomatic system with a language L.
I denote adding axioms W to a formal system S as S+W.
Definition The following defines in ZF [TODO: Anything changes if we allow stronger systems than ZF?] formal system with ordered types:
- A finite poset of types. [TODO: If infinite?]
- Finite numbers of functional symbols of finite arities.
- An infinite set of variables for each type.
- Terminal terms are functional symbols and variables.
- A designated binary functional symbol implication (⇒).
- A designated binary functional symbol equality (=). [TODO: Do we need to designate equality?]
- Each functional symbol is assigned a type and each functional symbol argument is assigned a type, each variable is assigned a type.
- We restrict considered formulas to such formulas where types of all symbol arguments are less than or equal the corresponding types of arguments.
- A (possibly infinite!) set of axioms (any formula can be an axiom).
- Substitution and modus ponens (defined for one of the binary functional symbols that we call implication).
Remark We need a possibly infinite set of axioms, because ZF is not finitely axiomatizable.
Note We have only functional, not relational symbols, and no logical symbols. Logical and relational symbols can be imitated by a functional symbol of a boolean type.
Think about types as sets of values and their order as set inclusion.
We will require that the system has a maximal type.
Not typed theories like ZF can be made typed by assigning all variables, functional symbols, and all arguments the same type (optionally to boolean expressions can be assigned a different type).
Formulas in a typed system is a subset of formulas in the corresponding untyped system. We will further take as obvious that for all our inference rules (see below), a proof in our typed system is the same as a proof in the corresponding untyped system with restriction that the formulas in the proof are conforming to the types.
Formal definition of inference rules
Definition A posed inference rule is a map F mapping finite sets of statements to sets of statements (provable by this rule).
Definition A composed posed inference rule C(S) for a finite set S of posed inference rules is defined as applying any finite sequence (including the empty sequence that is the identity mapping) of rules from S in any order with possible repetitions.
Definition An inference rules set S is a set of posed inference rules such that C(S)(X∪FX) = C(S)X for any set of statements X and posed inference rule FS. (In other words: applying a rule does not change the set of provable statements.)
Obvious The usual inference rules of the first-order logic (substitution, modus ponens, and universal generalization) in an inference rules set.
Definition An essential inference rules set is like inference rules set but equality is considered up to a bijective correspondence between symbols not present in X. (This definition is not used below.)
Definition I will say that a posed inference rule X does not create contradictions when added to a set of posed inference rules S, when false cannot be proved by C(S) implies false cannot be proven by C(S∪{X}).
Extension by definition
TODO: Say about conservative extensions.
Traditionally definitions introduce new symbols. In this system definitions instead take a symbol from a set to which the definition of the defined symbol are mapped as injection. Unlike traditional logic where definitions are considered shortcuts, in our logic definitions are considered theorems.
Remark To efficiently implement this in software, take as the value of the symbol a hash of the definition (plus a pointer to the definition stored in memory, to make the algorithm deterministic).
Thus if we define a symbol twice, it will be the same symbol, not two similarly defined symbols. This is essential to make definitions inference rules (as otherwise, after defining a symbol we lose the ability to define it again, what would make a definition not an inference rule).
Definition Simple extension by definition is adding a functional symbol f (of the same type as E) unambiguously determined by distinct variables x0, …, xn and an expression E in which no variables except of x0, …, xn are free, with adding f(x0, …, xn) = E as a proven formula.
Proposition Simple extension by definition does not create contradictions when added to {substitution, modus ponens, universal generalization} and is a conservative extension.
Proof Any occurrence of f can be replaced by E with appropriately substituted variables. For the added axiom it’s equivalent to E = E, for the rest formulas after substitution they are consequences of E = E. Thus no contradictions created and the extension is conservative.
Definition Functional extension by definition: distinct variables x0, …, xn, a formula P(y, x0, …, xn) for which the formula ∃!y:P(y, x0, …, xn) is proven; consider the functional symbol f determined by x0, …, xn and P and new proven formula P(f(x0, …, xn), x0, …, xn).
Theorem Functional extension by definition does not create contradictions when added to {substitution, modus ponens, universal generalization, simple extension by definition} and is a conservative extension.
Proof We are following [1]. (Adding types is trivial.) TODO: more detailed proof.
Theorem The usual inference rules of first-order logic together with the above defined variant of extension by definition are an inference rules set.
Proof We need to show that adding a definition does not diminish our ability to prove statements and add more definitions. It does not, because in our system defined symbols are not taken out of the set of symbols that can be used as names of new concepts.
Rule of modeling
Definition An unary functional symbol F is proven to be injective or provable injection when x:(Fx=Fy ⇒ x=y) is proven.
Definition We will denote (as defined in the customary first-order logic) the inverse of an injective functional symbol F as F-1.
Fix some formal system S and a proof.
Definition A modeled system S’ is:
- predicate P’ (expressing the set of elements of the model) [TODO: Predicates are not defined, we have only functional symbols.]
- a finite set F’ (functional symbols)
- designated binary functional symbol implication (⇒)
- a finite set of statements A’ containing only these symbols (expressing axioms of the modeled system)
Definition A modeled system S’ s modelable in S when
- there is a proven to be injective map I (let call the map model insertion) from S to S’. (For this to work, S needs to have a maximal type.)
- for every predefined functional symbol F, there is a functional symbol F’ (unambiguously defined by P, F, and I) of the modeled system such that is provedx0, …, xn P’:F’(x0, …, xn) = I-1F(Ix0, …, Ixn).
- Implication is mapped to the designated implication.
- Every axiom A’ is mapped by the replacement F’(x0, …, xn) → I-1F(Ix0, …, Ixn) into a proved statement.
Example ZF with Grothendieck universes is modelable in ZF.
Proof Let’s model in ZF ZF with proper classes. Such a model exists, because
Remark S’ can have any types (except that it has a maximal type).
Note that the property of being modelable is not the same as logical embedding. For example intuitionistic logic is modelable in classical logic, but isn’t embedded into it.
Definition A formal system S is provably embedded into a modeled system S’, when there exists a provable injection mapping every functional symbol of S into a functional symbol of S’ (mapping the implication to the implication) such that axioms of S’ are images of statements proven in S.
Example ZF is provably embedded into ZF with Grothendieck universes.
Definition S’ is self-modelable in S when S’ modelable and S is provably embedded into S’.
Proposition If S’’ is modelable in S’ and S’ is modelable in S, then S’’ is modelable in S.
Proof Compose the two model insertions. [??more detailed proof]
Corollary If S’’ is self-modelable in S’ and S’ is self-modelable in S, then S’’ is self-modelable in S.
Definition Model rule is replacing a formal system S by a formal system S’ where S’ is self-modelable in S.
Theorem Model rule together with standard inference rules and definition by extension is an inference rules set.
Proof Model rule does not in any way disturb to apply other rules.
Theorem Adding model rule inference rule does not make a non-contradictory formal system contradictory.
Proof ??
??Conservative extension.
Theorem Peano arithmetics with this additional inference rule can prove all axioms of ZFC with proper classes.
Proof Peano arithmetic can model ZF, ZF can model ZFC, ZFC can model proper classes through a Grothendieck universe.
So, I propose this new kind of logic as the new venue of mathematics.
An interesting philosophical implication is that in our system axiom of infinity is a theorem in Peano arithmetic. It raises the idea that existence of infinity can be scientifically or philosophically proved.
Moreover, embedding means that if we can model infinity in our logic, then infinite objects exists. It raises a philosophical argument that existence of potential infinity (infinity in model inside our formal system) implies existence of actual infinity (infinity in our formal system).
Conjecture Every non-contradictory formal system containing arithmetic together with model rule can prove its own non-contradictness.
This article added a new inference type to logic. We can add even more new inference rules. Say we can make A0, …, An |- NC(A0, …, An) a new inference rules, where NC means that a set of axioms is non-contradictory. It is needed if the previous conjecture is false.
Bibliography
[1] Wikipedia contributors, Extension by definitions, 22 October 2021 23:49 UTC, https://en.wikipedia.org/w/index.php?title=Extension_by_definitions&oldid=1051350724