**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 x_{0}, …, x_{n} and an expression E in which no variables except of x_{0}, …, x_{n} are free, with adding f(x_{0}, …, x_{n}) = 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** *Function**al extension by definition:* distinct variables x_{0}, …, x_{n}, a formula P(y, x_{0}, …, x_{n}) for which the formula ∃!y:P(y, x_{0}, …, x_{n}) is proven; consider the functional symbol f determined by x_{0}, …, x_{n} and P and new proven formula P(f(x_{0}, …, x_{n}), x_{0}, …, x_{n}).

**T****heorem** 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 provedx
_{0}, …, x_{n }P’:F’(x_{0}, …, x_{n}) = I^{-1}F(Ix_{0}, …, Ix_{n}). - Implication is mapped to the designated implication.
- Every axiom A’ is mapped by the replacement F’(x
_{0}, …, x_{n}) → I^{-1}F(Ix_{0}, …, Ix_{n}) into a proved statement.

**E****xample** ZF with Grothendieck universes is modelable in ZF.

**Proof** Let’s model in ZF ZF with proper classes. Such a model exists, because

**R****emark** 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.

**E****xample** 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 A_{0}, …, A_{n} |- NC(A_{0}, …, A_{n}) 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