NaturalNumberInductionRule
Attributes
- Source
- NaturalNumberInductionRule.scala
- Graph
-
- Supertypes
- Self type
Members list
Value members
Concrete methods
An LKProof ending with an induction over the natural numbers:
An LKProof ending with an induction over the natural numbers:
(π1) (π2)
Γ :- Δ, A[0] A[y], Π :- Λ, A[y]
------------------------------------ind
Γ, Π :- Δ, Λ, ∀x. A[x]
Note that there is an eigenvariable condition on x, i.e. x must not occur freely in Π :- Λ.
Value parameters
- aux1
-
The index of A[0].
- aux2
-
The index of A[y].
- aux3
-
The index of A[sy].
- leftSubProof
-
The subproof π,,1,,
- mainFormula
-
The formula ∀x. A[x].
- rightSubProof
-
The subproof π,,2,,
Attributes
An LKProof ending with an induction over the natural numbers:
An LKProof ending with an induction over the natural numbers:
(π1) (π2)
Γ :- Δ, A[0] A[y], Π :- Λ, A[y]
------------------------------------ind
Γ, Π :- Δ, Λ, ∀x. A[x]
Note that there is an eigenvariable condition on x, i.e. x must not occur freely in Π :- Λ.
Each of the aux formulas can be given as an index or a formula. If it is given as a formula, the constructor will attempt to find an appropriate index on its own.
Value parameters
- aux1
-
The index of A[0] or the formula itself.
- aux2
-
The index of A[y] or the formula itself.
- aux3
-
The index of A[sy] or the formula itself.
- leftSubProof
-
The subproof π,,1,,
- mainFormula
-
The formula ∀x. A[x].
- rightSubProof
-
The subproof π,,2,,
Attributes
Inherited methods
Attributes
- Inherited from:
- ConvenienceConstructor
- Source
- ConvenienceConstructor.scala
Inherited fields
Attributes
- Inherited from:
- ConvenienceConstructor
- Source
- ConvenienceConstructor.scala