diff --git a/src/main/scala/Example.scala b/src/main/scala/Example.scala
index a207d70a21196821ae8c6b4cea45c4817e3f18f8..dae950af9c5743fb50b6dc47743d8c581e1388d4 100644
--- a/src/main/scala/Example.scala
+++ b/src/main/scala/Example.scala
@@ -15,15 +15,9 @@ import utilities.tptp.*
*/
object Example {
def main(args: Array[String]): Unit = {
- // proofExample() //uncomment when exercise finished
+ proofExample() // uncomment when exercise finished
// solverExample()
// tptpExample()
-
- /*
- val a = ConstantPredicateLabel("a",0)
- val x = ConstantPredicateLabel("x",0)
- val r = isSame(iff(a(), a()), or(iff(a(), a()), x()))
- println(r)*/
}
/**
@@ -32,20 +26,24 @@ object Example {
* The last two lines don't need to be changed.
*/
def proofExample(): Unit = {
- val proof: SCProof = SCProof(
- Vector(
- ???,
- ???,
- ?????(Set(P(x), P(f(x)), P(f(x)) ==> P(f(f(x)))) |- P(f(f(x))), 1, 0, ????, ????),
- Hypothesis(Set(P(x), P(f(x)) ==> P(f(f(x)))) |- Set(P(x), P(f(f(x)))), P(x)),
- LeftImplies(???? |- ????, 3, 2, ????, ????),
- LeftForall(Set(????, ????, ????) |- ????, 4, ????, x, x),
- LeftForall(Set(????, ????) |- ????, 5, P(x) ==> P(f(x)), x, f(x)),
- RightImplies(forall(x, P(x) ==> P(f(x))) |- P(x) ==> P(f(f(x))), 6, P(x), P(f(f(x)))),
- RightForall(forall(x, P(x) ==> P(f(x))) |- forall(x, P(x) ==> P(f(f(x)))), 7, P(x) ==> P(f(f(x))), x)
- )
- )
- checkProof(proof)
+ object Ex extends proven.Main {
+ THEOREM("fixedPointDoubleApplication") of "" PROOF {
+ steps(
+ ???,
+ ???,
+ ?????(Set(P(x), P(f(x)), P(f(x)) ==> P(f(f(x)))) |- P(f(f(x))), 1, 0, ????, ????),
+ Hypothesis(Set(P(x), P(f(x)) ==> P(f(f(x)))) |- Set(P(x), P(f(f(x)))), P(x)),
+ LeftImplies(???? |- ????, 3, 2, ????, ????),
+ LeftForall(Set(????, ????, ????) |- ????, 4, ????, x, x),
+ LeftForall(Set(????, ????) |- ????, 5, P(x) ==> P(f(x)), x, f(x)),
+ RightImplies(forall(x, P(x) ==> P(f(x))) |- P(x) ==> P(f(f(x))), 6, P(x), P(f(f(x)))),
+ RightForall(forall(x, P(x) ==> P(f(x))) |- forall(x, P(x) ==> P(f(f(x)))), 7, P(x) ==> P(f(f(x))), x)
+ )
+ } using ()
+ show
+
+ }
+ Ex.main(Array(""))
}
/**
diff --git a/src/main/scala/lisa/kernel/proof/Judgement.scala b/src/main/scala/lisa/kernel/proof/Judgement.scala
index b0b86e27eeda5aa5d6ecba286a23f4572c32a388..e6fdb2f0e5c18ce53a53876e06233e5a2e45e832 100644
--- a/src/main/scala/lisa/kernel/proof/Judgement.scala
+++ b/src/main/scala/lisa/kernel/proof/Judgement.scala
@@ -71,6 +71,6 @@ object RunningTheoryJudgement {
* @param message The error message that hints about the first error encountered
*/
case class InvalidJustification[J <: RunningTheory#Justification](message: String, error: Option[SCProofCheckerJudgement.SCInvalidProof]) extends RunningTheoryJudgement[J]
-}
-case class InvalidJustificationException(message: String, error: Option[SCProofCheckerJudgement.SCInvalidProof]) extends Exception(message)
+ case class InvalidJustificationException(message: String, error: Option[SCProofCheckerJudgement.SCInvalidProof]) extends Exception(message)
+}
diff --git a/src/main/scala/lisa/kernel/proof/RunningTheory.scala b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
index 9d208036c13622a87b88528806f6d579a5ebe59b..ec979c1b856bed5bb4ead205ac5aeef9b1a44f38 100644
--- a/src/main/scala/lisa/kernel/proof/RunningTheory.scala
+++ b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
@@ -116,7 +116,7 @@ class RunningTheory {
* @param phi The formula defining the predicate.
* @return A definition object if the parameters are correct,
*/
- def makePredicateDefinition(label: ConstantPredicateLabel, expression:LambdaTermFormula): RunningTheoryJudgement[this.PredicateDefinition] = {
+ def makePredicateDefinition(label: ConstantPredicateLabel, expression: LambdaTermFormula): RunningTheoryJudgement[this.PredicateDefinition] = {
val LambdaTermFormula(vars, body) = expression
if (belongsToTheory(body))
if (isAvailable(label))
@@ -186,10 +186,17 @@ class RunningTheory {
val inner = ConnectorFormula(Iff, Seq(PredicateFormula(label, vars.map(FunctionTerm(_, Seq()))), body))
Sequent(Set(), Set(inner))
case FunctionDefinition(label, out, LambdaTermFormula(vars, body)) =>
- val inner = BinderFormula(Forall, out, ConnectorFormula(Iff, Seq(
- PredicateFormula(equality, Seq(FunctionTerm(label, vars.map(FunctionTerm.apply(_, Seq()))), VariableTerm(out))),
- body
- )))
+ val inner = BinderFormula(
+ Forall,
+ out,
+ ConnectorFormula(
+ Iff,
+ Seq(
+ PredicateFormula(equality, Seq(FunctionTerm(label, vars.map(FunctionTerm.apply(_, Seq()))), VariableTerm(out))),
+ body
+ )
+ )
+ )
Sequent(Set(), Set(inner))
}
diff --git a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala b/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
index d4f35c040e1758289fda2d37febeb382493086d0..8ecbc1f4827e61d04ed46cf0895f7371cf525e71 100644
--- a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
@@ -8,9 +8,8 @@ import utilities.Helpers.{_, given}
* Base trait for set theoretical axiom systems.
* Defines the symbols used in set theory.
*/
-trait SetTheoryDefinitions {
+private[settheory] trait SetTheoryDefinitions {
- private val tete = "tete"
def axioms: Set[(String, Formula)] = Set.empty
// Predicates
diff --git a/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
index 53e837d11ca738fc6b418408d9f9de86f0de0b28..ec50a16138395644ec1df0238f7c2e7d453fb7b0 100644
--- a/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
@@ -6,7 +6,7 @@ import utilities.Helpers.{_, given}
/**
* Axioms for the Tarski-Grothendieck theory (TG)
*/
-trait SetTheoryTGAxioms extends SetTheoryZFAxioms {
+private[settheory] trait SetTheoryTGAxioms extends SetTheoryZFAxioms {
private val (x, y, z) =
(VariableLabel("x"), VariableLabel("y"), VariableLabel("z"))
diff --git a/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
index 3e59d388a95ea5eeff19d435e9fc92634bbca78e..4d1dcbadaefeeca8f5c180b9c4407ec90482faa5 100644
--- a/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
@@ -7,7 +7,7 @@ import utilities.Helpers.{_, given}
/**
* Axioms for the Zermelo theory (Z)
*/
-trait SetTheoryZAxioms extends SetTheoryDefinitions {
+private[settheory] trait SetTheoryZAxioms extends SetTheoryDefinitions {
private val (x, y, z) =
(VariableLabel("x"), VariableLabel("y"), VariableLabel("z"))
diff --git a/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
index 50eaf462b6eb29d869a0564057c02a614be9fdc4..4cea73f78a46d2459f81978108cf326cee6d2238 100644
--- a/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
@@ -6,7 +6,7 @@ import utilities.Helpers.{_, given}
/**
* Axioms for the Zermelo-Fraenkel theory (ZF)
*/
-trait SetTheoryZFAxioms extends SetTheoryZAxioms {
+private[settheory] trait SetTheoryZFAxioms extends SetTheoryZAxioms {
private val (x, y, a, b) =
(VariableLabel("x"), VariableLabel("y"), VariableLabel("A"), VariableLabel("B"))
private final val sPsi = SchematicPredicateLabel("P", 3)
diff --git a/src/main/scala/proven/Main.scala b/src/main/scala/proven/Main.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7ee72a6ebb51b86c9ec723186368706616c726e3
--- /dev/null
+++ b/src/main/scala/proven/Main.scala
@@ -0,0 +1,19 @@
+package proven
+
+/**
+ * The parent trait of all theory files containing mathematical development
+ */
+trait Main {
+ export proven.SetTheoryLibrary.{*, given}
+
+ private val realOutput: String => Unit = println
+ private var outString: List[String] = List()
+ private val lineBreak = "\n"
+ given output: (String => Unit) = s => outString = lineBreak :: s :: outString
+
+ /**
+ * This specific implementation make sure that what is "shown" in theory files is only printed for the one we run, and not for the whole library.
+ */
+ def main(args: Array[String]): Unit = { realOutput(outString.reverse.mkString("")) }
+
+}
diff --git a/src/main/scala/proven/MainLibrary.scala b/src/main/scala/proven/MainLibrary.scala
deleted file mode 100644
index 31951ca0cce16881aa6297851cd2c5c1eb9853af..0000000000000000000000000000000000000000
--- a/src/main/scala/proven/MainLibrary.scala
+++ /dev/null
@@ -1,12 +0,0 @@
-package proven
-
-import lisa.kernel.proof.RunningTheory
-import lisa.settheory.AxiomaticSetTheory
-import lisa.settheory.SetTheoryDefinitions
-import utilities.Library
-
-abstract class MainLibrary extends Library(AxiomaticSetTheory.runningSetTheory) with SetTheoryDefinitions {
- import AxiomaticSetTheory.*
- override val realOutput: String => Unit = println
-
-}
diff --git a/src/main/scala/proven/SetTheory.scala b/src/main/scala/proven/SetTheory.scala
deleted file mode 100644
index 6279f36cc8020a8eb360ea380b9b43bc43c0ce85..0000000000000000000000000000000000000000
--- a/src/main/scala/proven/SetTheory.scala
+++ /dev/null
@@ -1,793 +0,0 @@
-package proven
-
-import lisa.kernel.fol.FOL.*
-import lisa.kernel.proof.RunningTheory
-import lisa.kernel.proof.RunningTheoryJudgement
-import lisa.kernel.proof.SequentCalculus.*
-import lisa.settheory.AxiomaticSetTheory
-import lisa.settheory.AxiomaticSetTheory.*
-import utilities.Helpers.{*, given}
-import proven.tactics.Destructors.*
-import proven.tactics.ProofTactics.*
-
-object SetTheory extends MainLibrary {
-
- THEOREM("russelParadox") of "∀x. (x ∈ ?y) ↔ ¬(x ∈ x) ⊢" PROOF {
- val y = SchematicFunctionLabel("y", 0)
- val x_ = VariableLabel("x")
- val contra = in(y, y) <=> !in(y, y)
- val s0 = Hypothesis(contra |- contra, contra)
- val s1 = LeftForall(forall(x_, in(x_, y) <=> !in(x_, x_)) |- contra, 0, in(x_, y) <=> !in(x_, x_), x_, y)
- val s2 = Rewrite(forall(x_, in(x_, y) <=> !in(x_, x_)) |- (), 1)
- Proof(s0, s1, s2)
- } using ()
- thm"russelParadox".show
-
- THEOREM("unorderedPair_symmetry") of
- "⊢ ∀y, x. {x, y} = {y, x}" PROOF {
- val x = VariableLabel("x")
- val y = VariableLabel("y")
- val z = VariableLabel("z")
- val h = SchematicPredicateLabel("h", 0)
- val fin = SCSubproof({
- val pr0 = SCSubproof({
- val pairSame11 = instantiateForall(new Proof(steps(), imports(ax"pairAxiom")), pairAxiom, x)
- val pairSame12 = instantiateForall(pairSame11, pairSame11.conclusion.right.head, y)
- instantiateForall(pairSame12, pairSame12.conclusion.right.head, z)
- }, Seq(-1))
- val pr1 = SCSubproof({
- val pairSame21 = instantiateForall(new Proof(steps(), imports(ax"pairAxiom")), pairAxiom, y)
- val pairSame22 = instantiateForall(pairSame21, pairSame21.conclusion.right.head, x)
- instantiateForall(pairSame22, pairSame22.conclusion.right.head, z)
- }, Seq(-1))
- val pr2 = RightSubstIff(
- Sequent(pr1.bot.right, Set(in(z, pair(x, y)) <=> in(z, pair(y, x)))),
- 0,
- List(((x === z) \/ (y === z), in(z, pair(y, x)))),
- LambdaFormulaFormula(Seq(h), in(z, pair(x, y)) <=> h())
- )
- val pr3 = Cut(Sequent(pr1.bot.left, pr2.bot.right), 1, 2, pr2.bot.left.head)
- val pr4 = RightForall(Sequent(Set(), Set(forall(z, pr2.bot.right.head))), 3, pr2.bot.right.head, z)
- Proof(steps(pr0, pr1, pr2, pr3, pr4), imports(ax"pairAxiom"))
- }, Seq(-2))
- val pairExt = SCSubproof({
- val pairExt1 = instantiateForall(Proof(steps(), imports(ax"extensionalityAxiom")), ax"extensionalityAxiom", pair(x, y))
- instantiateForall(pairExt1, pairExt1.conclusion.right.head, pair(y, x))
- }, Seq(-1))
- val fin2 = byEquiv(
- pairExt.bot.right.head,
- fin.bot.right.head
- )(pairExt, fin)
- val fin3 = generalizeToForall(fin2, fin2.conclusion.right.head, x)
- val fin4 = generalizeToForall(fin3, fin3.conclusion.right.head, y)
- fin4.copy(imports = imports(ax"extensionalityAxiom", ax"pairAxiom"))
- } using (ax"extensionalityAxiom", AxiomaticSetTheory.pairAxiom)
- show
-
- //This proof is old and very unoptimised
- THEOREM("unorderedPair_deconstruction") of
- "⊢ ∀x, y, x', y'. ({x, y} = {x', y'}) ⇒ (y' = y) ∧ (x' = x) ∨ (x = y') ∧ (y = x')" PROOF {
- val x = VariableLabel("x")
- val y = VariableLabel("y")
- val x1 = VariableLabel("x'")
- val y1 = VariableLabel("y'")
- val z = VariableLabel("z")
- val g = SchematicFunctionLabel("g", 0)
- val h = SchematicPredicateLabel("h", 0)
- val pxy = pair(x, y)
- val pxy1 = pair(x1, y1)
- val p0 = SCSubproof(
- {
- val p0 = SCSubproof(
- {
- val zf = in(z, pxy)
- val p1_0 = hypothesis(zf)
- val p1_1 = RightImplies(emptySeq +> (zf ==> zf), 0, zf, zf)
- val p1_2 = RightIff(emptySeq +> (zf <=> zf), 1, 1, zf, zf) // |- (z in {x,y} <=> z in {x,y})
- val p1_3 = RightSubstEq(emptySeq +< (pxy === pxy1) +> (zf <=> in(z, pxy1)), 2, List((pxy, pxy1)), LambdaTermFormula(Seq(g), zf <=> in(z, g())))
- Proof(IndexedSeq(p1_0, p1_1, p1_2, p1_3), IndexedSeq(() |- pairAxiom))
- },
- Seq(-1),
- display = true
- ) // ({x,y}={x',y'}) |- ((z∈{x,y})↔(z∈{x',y'}))
- val p1 = SCSubproof(
- {
- val p1_0 = Rewrite(() |- pairAxiom, -1) // |- ∀∀∀((z$1∈{x$3,y$2})↔((x$3=z$1)∨(y$2=z$1)))
- val p1_1 = instantiateForall(Proof(IndexedSeq(p1_0), IndexedSeq(() |- pairAxiom)), x, y, z)
- p1_1
- },
- Seq(-1),
- display = true
- ) // |- (z in {x,y}) <=> (z=x \/ z=y)
- val p2 = SCSubproof(
- {
- val p2_0 = Rewrite(() |- pairAxiom, -1) // |- ∀∀∀((z$1∈{x$3,y$2})↔((x$3=z$1)∨(y$2=z$1)))
- val p2_1 = instantiateForall(Proof(IndexedSeq(p2_0), IndexedSeq(() |- pairAxiom)), x1, y1, z)
- p2_1
- },
- Seq(-1),
- ) // |- (z in {x',y'}) <=> (z=x' \/ z=y')
- val p3 = RightSubstEq(
- emptySeq +< (pxy === pxy1) +> (in(z, pxy1) <=> ((z === x) \/ (z === y))),
- 1,
- List((pxy, pxy1)),
- LambdaTermFormula(Seq(g), in(z, g()) <=> ((z === x) \/ (z === y)))
- ) // ({x,y}={x',y'}) |- ((z∈{x',y'})↔((z=x)∨(z=y)))
- val p4 = RightSubstIff(
- emptySeq +< p3.bot.left.head +< p2.bot.right.head +> (((z === x) \/ (z === y)) <=> ((z === x1) \/ (z === y1))),
- 3,
- List(((z === x1) \/ (z === y1), in(z, pxy1))),
- LambdaFormulaFormula(Seq(h), h() <=> ((z === x) \/ (z === y)))
- ) // ((z∈{x',y'})↔((x'=z)∨(y'=z))), ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
- val p5 = Cut(emptySeq ++< p3.bot ++> p4.bot, 2, 4, p2.bot.right.head)
- Proof(IndexedSeq(p0, p1, p2, p3, p4, p5), IndexedSeq(() |- pairAxiom))
- },
- Seq(-1)
- ) // ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
-
- val p1 = SCSubproof(
- Proof(
- byCase(x === x1)(
- SCSubproof(
- {
- val pcm1 = p0
- val pc0 = SCSubproof(
- Proof(
- byCase(y === x)(
- SCSubproof(
- {
- val pam1 = pcm1
- val pa0 = SCSubproof(
- {
- val f1 = z === x
- val pa0_m1 = pcm1 // ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
- val pa0_0 = SCSubproof(
- {
- val pa0_0_0 = hypothesis(f1)
- val pa0_1_1 = RightOr(emptySeq +< f1 +> (f1 \/ f1), 0, f1, f1)
- val pa0_1_2 = RightImplies(emptySeq +> (f1 ==> (f1 \/ f1)), 1, f1, f1 \/ f1)
- val pa0_1_3 = LeftOr(emptySeq +< (f1 \/ f1) +> f1, Seq(0, 0), Seq(f1, f1))
- val pa0_1_4 = RightImplies(emptySeq +> ((f1 \/ f1) ==> f1), 3, f1 \/ f1, f1)
- val pa0_1_5 = RightIff(emptySeq +> ((f1 \/ f1) <=> f1), 2, 4, (f1 \/ f1), f1)
- val r = Proof(pa0_0_0, pa0_1_1, pa0_1_2, pa0_1_3, pa0_1_4, pa0_1_5)
- r
- },
- display = false
- ) // |- (((z=x)∨(z=x))↔(z=x))
- val pa0_1 = RightSubstEq(
- emptySeq +< (pxy === pxy1) +< (x === y) +> ((f1 \/ f1) <=> (z === x1) \/ (z === y1)),
- -1,
- List((x, y)),
- LambdaTermFormula(Seq(g), (f1 \/ (z === g())) <=> ((z === x1) \/ (z === y1)))
- ) // ({x,y}={x',y'}) y=x|- (z=x)\/(z=x) <=> (z=x' \/ z=y')
- val pa0_2 = RightSubstIff(
- emptySeq +< (pxy === pxy1) +< (x === y) +< (f1 <=> (f1 \/ f1)) +> (f1 <=> ((z === x1) \/ (z === y1))),
- 1,
- List((f1, f1 \/ f1)),
- LambdaFormulaFormula(Seq(h), h() <=> ((z === x1) \/ (z === y1)))
- )
- val pa0_3 =
- Cut(emptySeq +< (pxy === pxy1) +< (x === y) +> (f1 <=> ((z === x1) \/ (z === y1))), 0, 2, f1 <=> (f1 \/ f1)) // (x=y), ({x,y}={x',y'}) |- ((z=x)↔((z=x')∨(z=y')))
- val pa0_4 = RightForall(emptySeq +< (pxy === pxy1) +< (x === y) +> forall(z, f1 <=> ((z === x1) \/ (z === y1))), 3, f1 <=> ((z === x1) \/ (z === y1)), z)
- val ra0_0 = instantiateForall(Proof(IndexedSeq(pa0_0, pa0_1, pa0_2, pa0_3, pa0_4), IndexedSeq(pa0_m1.bot)), y1) // (x=y), ({x,y}={x',y'}) |- ((y'=x)↔((y'=x')∨(y'=y')))
- ra0_0
- },
- IndexedSeq(-1)
- ) // ({x,y}={x',y'}) y=x|- ((y'=x)↔((y'=x')∨(y'=y')))
- val pa1 = SCSubproof(
- {
- val pa1_0 = RightRefl(emptySeq +> (y1 === y1), y1 === y1)
- val pa1_1 = RightOr(emptySeq +> ((y1 === y1) \/ (y1 === x1)), 0, y1 === y1, y1 === x1)
- Proof(pa1_0, pa1_1)
- },
- display = false
- ) // |- (y'=x' \/ y'=y')
- val ra3 = byEquiv(pa0.bot.right.head, pa1.bot.right.head)(pa0, pa1) // ({x,y}={x',y'}) y=x|- ((y'=x)
- val pal = RightSubstEq(emptySeq ++< pa0.bot +> (y1 === y), ra3.length - 1, List((x, y)), LambdaTermFormula(Seq(g), y1 === g()))
- Proof(ra3.steps, IndexedSeq(pam1.bot)).appended(pal) // (x=y), ({x,y}={x',y'}) |- (y'=y)
- },
- IndexedSeq(-1)
- ) // (x=y), ({x,y}={x',y'}) |- (y'=y)
- ,
- SCSubproof(
- {
- val pbm1 = pcm1 // ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
- val pb0_0 = SCSubproof(
- {
- val pb0_0 = RightForall(emptySeq ++< pcm1.bot +> forall(z, pcm1.bot.right.head), -1, pcm1.bot.right.head, z)
- instantiateForall(Proof(IndexedSeq(pb0_0), IndexedSeq(pcm1.bot)), y)
- },
- IndexedSeq(-1)
- ) // ({x,y}={x',y'}) |- (((y=x)∨(y=y))↔((y=x')∨(y=y')))
- val pb0_1 = SCSubproof(
- {
- val pa1_0 = RightRefl(emptySeq +> (y === y), y === y)
- val pa1_1 = RightOr(emptySeq +> ((y === y) \/ (y === x)), 0, y === y, y === x)
- Proof(pa1_0, pa1_1)
- },
- display = false
- ) // |- (y=x)∨(y=y)
- val rb0 = byEquiv(pb0_0.bot.right.head, pb0_1.bot.right.head)(pb0_0, pb0_1) // ({x,y}={x',y'}) |- (y=x')∨(y=y')
- val pb1 =
- RightSubstEq(emptySeq ++< rb0.conclusion +< (x === x1) +> ((y === x) \/ (y === y1)), rb0.length - 1, List((x, x1)), LambdaTermFormula(Seq(g), (y === g()) \/ (y === y1)))
- val rb1 = destructRightOr(
- rb0.appended(pb1), // ({x,y}={x',y'}) , x=x'|- (y=x)∨(y=y')
- y === x,
- y === y1
- )
- val rb2 = rb1.appended(LeftNot(rb1.conclusion +< !(y === x) -> (y === x), rb1.length - 1, y === x)) // (x=x'), ({x,y}={x',y'}), ¬(y=x) |- (y=y')
- Proof(rb2.steps, IndexedSeq(pbm1.bot))
-
- },
- IndexedSeq(-1)
- ) // ({x,y}={x',y'}), x=x', !y=x |- y=y'
- ).steps,
- IndexedSeq(pcm1.bot)
- ),
- IndexedSeq(-1)
- ) // (x=x'), ({x,y}={x',y'}) |- (y'=y)
- val pc1 = RightRefl(emptySeq +> (x === x), x === x)
- val pc2 = RightAnd(emptySeq ++< pc0.bot +> ((y1 === y) /\ (x === x)), Seq(0, 1), Seq(y1 === y, x === x)) // ({x,y}={x',y'}), x=x' |- (x=x /\ y=y')
- val pc3 =
- RightSubstEq(emptySeq ++< pc2.bot +> ((y1 === y) /\ (x1 === x)), 2, List((x, x1)), LambdaTermFormula(Seq(g), (y1 === y) /\ (g() === x))) // ({x,y}={x',y'}), x=x' |- (x=x' /\ y=y')
- val pc4 = RightOr(
- emptySeq ++< pc3.bot +> (pc3.bot.right.head \/ ((x === y1) /\ (y === x1))),
- 3,
- pc3.bot.right.head,
- (x === y1) /\ (y === x1)
- ) // ({x,y}={x',y'}), x=x' |- (x=x' /\ y=y')\/(x=y' /\ y=x')
- val r = Proof(IndexedSeq(pc0, pc1, pc2, pc3, pc4), IndexedSeq(pcm1.bot))
- r
- },
- IndexedSeq(-1)
- ) // ({x,y}={x',y'}), x=x' |- (x=x' /\ y=y')\/(x=y' /\ y=x')
- ,
- SCSubproof(
- {
- val pdm1 = p0
- val pd0 = SCSubproof(
- {
- val pd0_m1 = pdm1
- val pd0_0 = SCSubproof {
- val ex1x1 = x1 === x1
- val pd0_0_0 = RightRefl(emptySeq +> ex1x1, ex1x1) // |- x'=x'
- val pd0_0_1 = RightOr(emptySeq +> (ex1x1 \/ (x1 === y1)), 0, ex1x1, x1 === y1) // |- (x'=x' \/ x'=y')
- Proof(IndexedSeq(pd0_0_0, pd0_0_1))
- } // |- (x'=x' \/ x'=y')
- val pd0_1 = SCSubproof(
- {
- val pd0_1_m1 = pd0_m1 // ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
- val pd0_1_0 = RightForall(emptySeq ++< pd0_1_m1.bot +> forall(z, pd0_1_m1.bot.right.head), -1, pd0_1_m1.bot.right.head, z)
- val rd0_1_1 = instantiateForall(Proof(IndexedSeq(pd0_1_0), IndexedSeq(pd0_m1.bot)), x1) // ({x,y}={x',y'}) |- (x'=x \/ x'=y) <=> (x'=x' \/ x'=y')
- rd0_1_1
- },
- IndexedSeq(-1)
- ) // ({x,y}={x',y'}) |- (x'=x \/ x'=y) <=> (x'=x' \/ x'=y')
- val pd0_2 = RightSubstIff(
- pd0_1.bot.right |- ((x1 === x) \/ (x1 === y)),
- 0,
- List(((x1 === x) \/ (x1 === y), (x1 === x1) \/ (x1 === y1))),
- LambdaFormulaFormula(Seq(h), h())
- ) // (x'=x \/ x'=y) <=> (x'=x' \/ x'=y') |- (x'=x \/ x'=y)
- val pd0_3 = Cut(pd0_1.bot.left |- pd0_2.bot.right, 1, 2, pd0_1.bot.right.head) // ({x,y}={x',y'}) |- (x=x' \/ y=x')
- destructRightOr(Proof(IndexedSeq(pd0_0, pd0_1, pd0_2, pd0_3), IndexedSeq(pd0_m1.bot)), x === x1, y === x1) // ({x,y}={x',y'}) |- x=x', y=x'
- },
- IndexedSeq(-1)
- ) // ({x,y}={x',y'}) |- x=x', y=x' --
- val pd1 = SCSubproof(
- {
- val pd1_m1 = pdm1
- val pd1_0 = SCSubproof {
- val exx = x === x
- val pd1_0_0 = RightRefl(emptySeq +> exx, exx) // |- x=x
- val pd1_0_1 = RightOr(emptySeq +> (exx \/ (x === y)), 0, exx, x === y) // |- (x=x \/ x=y)
- Proof(IndexedSeq(pd1_0_0, pd1_0_1))
- } // |- (x=x \/ x=y)
- val pd1_1 = SCSubproof(
- {
- val pd1_1_m1 = pd1_m1 // ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
- val pd1_1_0 = RightForall(emptySeq ++< pd1_1_m1.bot +> forall(z, pd1_1_m1.bot.right.head), -1, pd1_1_m1.bot.right.head, z)
- val rd1_1_1 = instantiateForall(Proof(IndexedSeq(pd1_1_0), IndexedSeq(pd1_m1.bot)), x) // ({x,y}={x',y'}) |- (x=x \/ x=y) <=> (x=x' \/ x=y')
- rd1_1_1
- },
- IndexedSeq(-1)
- ) // // ({x,y}={x',y'}) |- (x=x \/ x=y) <=> (x=x' \/ x=y')
- val rd1_2 = byEquiv(pd1_1.bot.right.head, pd1_0.bot.right.head)(pd1_1, pd1_0)
- val pd1_3 = SCSubproof(Proof(rd1_2.steps, IndexedSeq(pd1_m1.bot)), IndexedSeq(-1)) // // ({x,y}={x',y'}) |- x=x' \/ x=y'
- destructRightOr(Proof(IndexedSeq(pd1_0, pd1_1, pd1_3), IndexedSeq(pd1_m1.bot)), x === x1, x === y1) // ({x,y}={x',y'}) |- x=x', x=y'
- },
- IndexedSeq(-1)
- ) // ({x,y}={x',y'}) |- x=x', x=y' --
- val pd2 = RightAnd(emptySeq ++< pd1.bot +> (x === x1) +> ((x === y1) /\ (y === x1)), Seq(0, 1), Seq(x === y1, y === x1)) // ({x,y}={x',y'}) |- x=x', (x=y' /\ y=x') ---
- val pd3 = LeftNot(emptySeq ++< pd2.bot +< !(x === x1) +> ((x === y1) /\ (y === x1)), 2, x === x1) // ({x,y}={x',y'}), !x===x1 |- (x=y' /\ y=x')
- val pd4 = RightOr(
- emptySeq ++< pd3.bot +> (pd3.bot.right.head \/ ((x === x1) /\ (y === y1))),
- 3,
- pd3.bot.right.head,
- (x === x1) /\ (y === y1)
- ) // ({x,y}={x',y'}), !x===x1 |- (x=x' /\ y=y')\/(x=y' /\ y=x')
- Proof(IndexedSeq(pd0, pd1, pd2, pd3, pd4), IndexedSeq(pdm1.bot))
- },
- IndexedSeq(-1)
- ) // ({x,y}={x',y'}), !x=x' |- (x=x' /\ y=y')\/(x=y' /\ y=x')
- ).steps,
- IndexedSeq(p0.bot)
- ),
- IndexedSeq(0)
- ) // ({x,y}={x',y'}) |- (x=x' /\ y=y')\/(x=y' /\ y=x')
-
- val p2 = RightImplies(emptySeq +> (p1.bot.left.head ==> p1.bot.right.head), 1, p1.bot.left.head, p1.bot.right.head) // |- ({x,y}={x',y'}) ==> (x=x' /\ y=y')\/(x=y' /\ y=x')
- generalizeToForall(Proof(IndexedSeq(p0, p1, p2), IndexedSeq(() |- pairAxiom)), x, y, x1, y1)
- } using ax"pairAxiom"
- thm"unorderedPair_deconstruction".show
-
- THEOREM("noUniversalSet") of "∀x. x ∈ ?z ⊢" PROOF {
- val x = SchematicFunctionLabel("x", 0)
- val z = SchematicFunctionLabel("z", 0)
- val x1 = VariableLabel("x")
- val y1 = VariableLabel("y")
- val z1 = VariableLabel("z")
- val h = SchematicPredicateLabel("h", 0)
- val sPhi = SchematicPredicateLabel("P", 2)
- // forall(z, exists(y, forall(x, in(x,y) <=> (in(x,y) /\ sPhi(x,z)))))
- val i1 = () |- comprehensionSchema
- val i2 = thm"russelParadox" // forall(x1, in(x1,y) <=> !in(x1, x1)) |- ()
- val p0 = InstPredSchema(() |- forall(z1, exists(y1, forall(x1, in(x1, y1) <=> (in(x1, z1) /\ !in(x1, x1))))), -1, Map(sPhi -> LambdaTermFormula(Seq(x, z), !in(x(), x()))))
- val s0 = SCSubproof(instantiateForall(Proof(IndexedSeq(p0), IndexedSeq(i1)), z), Seq(-1)) // exists(y1, forall(x1, in(x1,y1) <=> (in(x1,z1) /\ !in(x1, x1))))
- val s1 = hypothesis(in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1))) // in(x,y) <=> (in(x,z) /\ in(x, x)) |- in(x,y) <=> (in(x,z) /\ in(x, x))
- val s2 = RightSubstIff(
- (in(x1, z) <=> And(), in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1))) |- in(x1, y1) <=> (And() /\ !in(x1, x1)),
- 1,
- List((in(x1, z), And())),
- LambdaFormulaFormula(Seq(h), in(x1, y1) <=> (h() /\ !in(x1, x1)))
- ) // in(x1,y1) <=> (in(x1,z1) /\ in(x1, x1)) |- in(x,y) <=> (And() /\ in(x1, x1))
- val s3 = Rewrite((in(x1, z), in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1))) |- in(x1, y1) <=> !in(x1, x1), 2)
- val s4 = LeftForall((forall(x1, in(x1, z)), in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1))) |- in(x1, y1) <=> !in(x1, x1), 3, in(x1, z), x1, x1)
- val s5 = LeftForall((forall(x1, in(x1, z)), forall(x1, in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1)))) |- in(x1, y1) <=> !in(x1, x1), 4, in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1)), x1, x1)
- val s6 = RightForall((forall(x1, in(x1, z)), forall(x1, in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1)))) |- forall(x1, in(x1, y1) <=> !in(x1, x1)), 5, in(x1, y1) <=> !in(x1, x1), x1)
- val s7 = InstFunSchema(forall(x1, in(x1, y1) <=> !in(x1, x1)) |- (), -2, Map(SchematicFunctionLabel("y", 0) -> LambdaTermTerm(Nil, y1)))
- val s8 = Cut((forall(x1, in(x1, z)), forall(x1, in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1)))) |- (), 6, 7, forall(x1, in(x1, y1) <=> !in(x1, x1)))
- val s9 = LeftExists((forall(x1, in(x1, z)), exists(y1, forall(x1, in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1))))) |- (), 8, forall(x1, in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1))), y1)
- val s10 = Cut(forall(x1, in(x1, z)) |- (), 0, 9, exists(y1, forall(x1, in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1)))))
- Proof(steps(s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10), imports(i1, i2))
- } using (ax"comprehensionSchema", thm"russelParadox")
- show
-
- private val sx = SchematicFunctionLabel("x", 0)
- private val sy = SchematicFunctionLabel("y", 0)
- val oPair: ConstantFunctionLabel = DEFINE("", sx, sy) as pair(pair(sx, sy), pair(sx, sx))
- show
-
- THEOREM("functionalMapping") of
- "∀a. (a ∈ ?A) ⇒ ∃!x. ?phi(x, a) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ ?A) ∧ ?phi(x, a)" PROOF {
- val a = VariableLabel("a")
- val b = VariableLabel("b")
- val x = VariableLabel("x")
- val y = VariableLabel("y")
- val z = VariableLabel("z")
- val a1 = SchematicFunctionLabel("a", 0)
- val b1 = SchematicFunctionLabel("b", 0)
- val x1 = SchematicFunctionLabel("x", 0)
- val y1 = SchematicFunctionLabel("y", 0)
- val z1 = SchematicFunctionLabel("z", 0)
- val f = SchematicFunctionLabel("f", 0)
- val h = SchematicPredicateLabel("h", 0)
- val A = SchematicFunctionLabel("A", 0)()
- val X = VariableLabel("X")
- val B = VariableLabel("B")
- val B1 = VariableLabel("B1")
- val phi = SchematicPredicateLabel("phi", 2)
- val sPhi = SchematicPredicateLabel("P", 2)
- val sPsi = SchematicPredicateLabel("P", 3)
-
- val H = existsOne(x, phi(x, a))
- val H1 = forall(a, in(a, A) ==> H)
- val s0 = hypothesis(H) // () |- existsOne(x, phi(x, a)))
- val s1 = Weakening((H, in(a, A)) |- existsOne(x, phi(x, a)), 0)
- val s2 = Rewrite((H) |- in(a, A) ==> existsOne(x, phi(x, a)), 1)
- // val s3 = RightForall((H) |- forall(a, in(a, A) ==> existsOne(x, phi(x, a))), 2, in(a, A) ==> existsOne(x, phi(x, a)), a) // () |- ∀a∈A. ∃!x. phi(x, a)
- val s3 = hypothesis(H1)
- val i1 = () |- replacementSchema
- val p0 = InstPredSchema(
- () |- instantiatePredicateSchemas(replacementSchema, Map(sPsi -> LambdaTermFormula(Seq(y1, a1, x1), phi(x1, a1)))),
- -1,
- Map(sPsi -> LambdaTermFormula(Seq(y1, a1, x1), phi(x1, a1)))
- )
- val p1 = instantiateForall(Proof(steps(p0), imports(i1)), A)
- val s4 = SCSubproof(p1, Seq(-1)) //
- val s5 = Rewrite(s3.bot.right.head |- exists(B, forall(x, in(x, A) ==> exists(y, in(y, B) /\ (phi(y, x))))), 4)
- val s6 = Cut((H1) |- exists(B, forall(x, in(x, A) ==> exists(y, in(y, B) /\ (phi(y, x))))), 3, 5, s3.bot.right.head) // ⊢ ∃B. ∀x. (x ∈ A) ⇒ ∃y. (y ∈ B) ∧ (y = (x, b))
-
- val i2 = () |- comprehensionSchema // forall(z, exists(y, forall(x, in(x,y) <=> (in(x,z) /\ sPhi(x,z)))))
- val q0 = InstPredSchema(
- () |- instantiatePredicateSchemas(comprehensionSchema, Map(sPhi -> LambdaTermFormula(Seq(x1, z1), exists(a, in(a, A) /\ phi(x1, a))))),
- -1,
- Map(sPhi -> LambdaTermFormula(Seq(x1, z1), exists(a, in(a, A) /\ phi(x1, a))))
- )
- val q1 = instantiateForall(Proof(steps(q0), imports(i2)), B)
- val s7 = SCSubproof(q1, Seq(-2)) // ∃y. ∀x. (x ∈ y) ↔ (x ∈ B) ∧ ∃a. a ∈ A /\ x = (a, b) := exists(y, F(y) )
- Proof(steps(s0, s1, s2, s3, s4, s5, s6, s7), imports(i1, i2))
- val s8 = SCSubproof({
- val y1 = VariableLabel("y1")
- val f = SchematicFunctionLabel("f", 0)
- val s0 = hypothesis(in(y1, B))
- val s1 = RightSubstEq((in(y1, B), x === y1) |- in(x, B), 0, List((x, y1)), LambdaTermFormula(Seq(f), in(f(), B)))
- val s2 = LeftSubstIff(Set(in(y1, B), (x === y1) <=> phi(x, a), phi(x, a)) |- in(x, B), 1, List(((x === y1), phi(x, a))), LambdaFormulaFormula(Seq(h), h()))
- val s3 = LeftSubstEq(Set(y === y1, in(y1, B), (x === y) <=> phi(x, a), phi(x, a)) |- in(x, B), 2, List((y, y1)), LambdaTermFormula(Seq(f), (x === f()) <=> phi(x, a)))
- val s4 = LeftSubstIff(Set((y === y1) <=> phi(y1, a), phi(y1, a), in(y1, B), (x === y) <=> phi(x, a), phi(x, a)) |- in(x, B), 3, List((phi(y1, a), y1 === y)), LambdaFormulaFormula(Seq(h), h()))
- val s5 = LeftForall(Set(forall(x, (y === x) <=> phi(x, a)), phi(y1, a), in(y1, B), (x === y) <=> phi(x, a), phi(x, a)) |- in(x, B), 4, (y === x) <=> phi(x, a), x, y1)
- val s6 = LeftForall(Set(forall(x, (y === x) <=> phi(x, a)), phi(y1, a), in(y1, B), phi(x, a)) |- in(x, B), 5, (x === y) <=> phi(x, a), x, x)
- val s7 = LeftExists(Set(exists(y, forall(x, (y === x) <=> phi(x, a))), phi(y1, a), in(y1, B), phi(x, a)) |- in(x, B), 6, forall(x, (y === x) <=> phi(x, a)), y)
- val s8 = Rewrite(Set(exists(y, forall(x, (y === x) <=> phi(x, a))), phi(y1, a) /\ in(y1, B), phi(x, a)) |- in(x, B), 7)
- val s9 = LeftExists(Set(exists(y, forall(x, (y === x) <=> phi(x, a))), exists(y1, phi(y1, a) /\ in(y1, B)), phi(x, a)) |- in(x, B), 8, phi(y1, a) /\ in(y1, B), y1)
- val s10 = Rewrite(Set(exists(y, forall(x, (y === x) <=> phi(x, a))), And() ==> exists(y, phi(y, a) /\ in(y, B)), phi(x, a)) |- in(x, B), 9)
- val s11 = LeftSubstIff(
- Set(exists(y, forall(x, (y === x) <=> phi(x, a))), in(a, A) ==> exists(y, phi(y, a) /\ in(y, B)), phi(x, a), in(a, A)) |- in(x, B),
- 10,
- List((And(), in(a, A))),
- LambdaFormulaFormula(Seq(h), h() ==> exists(y, phi(y, a) /\ in(y, B)))
- )
- val s12 = LeftForall(
- Set(exists(y, forall(x, (y === x) <=> phi(x, a))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a), in(a, A)) |- in(x, B),
- 11,
- in(a, A) ==> exists(y, phi(y, a) /\ in(y, B)),
- a,
- a
- )
- val s13 = LeftSubstIff(
- Set(in(a, A) ==> exists(y, forall(x, (y === x) <=> phi(x, a))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a), in(a, A)) |- in(x, B),
- 12,
- List((And(), in(a, A))),
- LambdaFormulaFormula(Seq(h), h() ==> exists(y, forall(x, (y === x) <=> phi(x, a))))
- )
- val s14 = LeftForall(
- Set(forall(a, in(a, A) ==> exists(y, forall(x, (y === x) <=> phi(x, a)))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a), in(a, A)) |- in(x, B),
- 13,
- in(a, A) ==> exists(y, forall(x, (y === x) <=> phi(x, a))),
- a,
- a
- )
- val s15 = Rewrite(Set(forall(a, in(a, A) ==> exists(y, forall(x, (y === x) <=> phi(x, a)))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a) /\ in(a, A)) |- in(x, B), 14)
- val s16 = LeftExists(
- Set(forall(a, in(a, A) ==> exists(y, forall(x, (y === x) <=> phi(x, a)))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), exists(a, phi(x, a) /\ in(a, A))) |- in(x, B),
- 15,
- phi(x, a) /\ in(a, A),
- a
- )
- val truc = forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B)))
- val s17 = Rewrite(Set(forall(a, in(a, A) ==> existsOne(x, phi(x, a))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), exists(a, phi(x, a) /\ in(a, A))) |- in(x, B), 16)
- Proof(steps(s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, s17))
- // goal H, ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B)
- // redGoal ∀a.(a ∈ A) => ∃!x. phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B) s17
- // redGoal ∀a.(a ∈ A) => ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B) s16
- // redGoal ∀a.(a ∈ A) => ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A ∧ phi(x, a) |- (x ∈ B) s15
- // redGoal ∀a.(a ∈ A) => ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A, phi(x, a) |- (x ∈ B) s14
- // redGoal (a ∈ A) => ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A, phi(x, a) |- (x ∈ B) s13
- // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A, phi(x, a) |- (x ∈ B) s12
- // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A, phi(x, a) |- (x ∈ B) s11
- // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A <=> T, phi(x, a) |- (x ∈ B) s11
- // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), T ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A <=> T, phi(x, a) |- (x ∈ B) s10
- // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), ∃y1. y1 ∈ B ∧ phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s9
- // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), y1 ∈ B ∧ phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s8
- // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), y1 ∈ B, phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s7
- // redGoal ∀x. (x=y) ↔ phi(x, a), y1 ∈ B, phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s6
- // redGoal (x=y) ↔ phi(x, a), ∀x. (x=y) ↔ phi(x, a), y1 ∈ B, phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s5
- // redGoal (x=y) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s4
- // redGoal (x=y) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, (y1=y), a ∈ A, phi(x, a) |- (x ∈ B) s3
- // redGoal (x=y1) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, (y1=y), a ∈ A, phi(x, a) |- (x ∈ B) s2
- // redGoal (x=y1) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, (y1=y), a ∈ A, x=y1 |- (x ∈ B) s1
- // redGoal (x=y1) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, (y1=y), a ∈ A, x=y1 |- (y1 ∈ B) s0
-
- }) // H, ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B)
-
- val G = forall(a, in(a, A) ==> exists(y, in(y, B) /\ (phi(y, a))))
- val F = forall(x, iff(in(x, B1), in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a)))))
- val s9 = SCSubproof({
- val p0 = instantiateForall(Proof(hypothesis(F)), x)
- val left = in(x, B1)
- val right = in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a)))
- val p1 = p0.withNewSteps(Vector(Rewrite(F |- (left ==> right) /\ (right ==> left), p0.length - 1)))
- val p2 = destructRightAnd(p1, (right ==> left), (left ==> right)) // F |- in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a))) => in(x, B1)
- val p3 = p2.withNewSteps(Vector(Rewrite(Set(F, in(x, B), exists(a, in(a, A) /\ (phi(x, a)))) |- in(x, B1), p2.length - 1)))
- p3
- }) // have F, (x ∈ B), ∃a. a ∈ A ∧ x = (a, b) |- (x ∈ B1)
- val s10 = Cut(Set(F, G, H1, exists(a, in(a, A) /\ (phi(x, a)))) |- in(x, B1), 8, 9, in(x, B)) // redGoal F, ∃a. a ∈ A ∧ x = (a, b), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ y = (a, b) |- (x ∈ B1)
- val s11 = Rewrite(Set(H1, G, F) |- exists(a, in(a, A) /\ (phi(x, a))) ==> in(x, B1), 10) // F |- ∃a. a ∈ A ∧ x = (a, b) => (x ∈ B1) --- half
- val s12 = SCSubproof({
- val p0 = instantiateForall(Proof(hypothesis(F)), x)
- val left = in(x, B1)
- val right = in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a)))
- val p1 = p0.withNewSteps(Vector(Rewrite(F |- (left ==> right) /\ (right ==> left), p0.length - 1)))
- val p2 = destructRightAnd(p1, (left ==> right), (right ==> left)) // F |- in(x, B1) => in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a))) =>
- val p3 = p2.withNewSteps(Vector(Rewrite(Set(F, in(x, B1)) |- exists(a, in(a, A) /\ (phi(x, a))) /\ in(x, B), p2.length - 1)))
- val p4 = destructRightAnd(p3, exists(a, in(a, A) /\ (phi(x, a))), in(x, B))
- val p5 = p4.withNewSteps(Vector(Rewrite(F |- in(x, B1) ==> exists(a, in(a, A) /\ (phi(x, a))), p4.length - 1)))
- p5
- }) // have F |- (x ∈ B1) ⇒ ∃a. a ∈ A ∧ x = (a, b) --- other half
- val s13 = RightIff((H1, G, F) |- in(x, B1) <=> exists(a, in(a, A) /\ (phi(x, a))), 11, 12, in(x, B1), exists(a, in(a, A) /\ (phi(x, a)))) // have F |- (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
- val s14 =
- RightForall((H1, G, F) |- forall(x, in(x, B1) <=> exists(a, in(a, A) /\ (phi(x, a)))), 13, in(x, B1) <=> exists(a, in(a, A) /\ (phi(x, a))), x) // G, F |- ∀x. (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
-
- val i3 = () |- extensionalityAxiom
- val s15 = SCSubproof(
- {
- val i1 = s13.bot // G, F |- (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
- val i2 = () |- extensionalityAxiom
- val t0 = RightSubstIff(
- Set(H1, G, F, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))) |- in(x, X) <=> in(x, B1),
- -1,
- List((in(x, X), exists(a, in(a, A) /\ (phi(x, a))))),
- LambdaFormulaFormula(Seq(h), h() <=> in(x, B1))
- ) // redGoal2 F, (z ∈ X) <=> ∃a. a ∈ A ∧ z = (a, b) |- (z ∈ X) <=> (z ∈ B1)
- val t1 = LeftForall(
- Set(H1, G, F, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))) |- in(x, X) <=> in(x, B1),
- 0,
- in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))),
- x,
- x
- ) // redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] |- (z ∈ X) <=> (z ∈ B1)
- val t2 = RightForall(t1.bot.left |- forall(x, in(x, X) <=> in(x, B1)), 1, in(x, X) <=> in(x, B1), x) // redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] |- ∀z. (z ∈ X) <=> (z ∈ B1)
- val t3 =
- SCSubproof(instantiateForall(Proof(steps(Rewrite(() |- extensionalityAxiom, -1)), imports(() |- extensionalityAxiom)), X, B1), Vector(-2)) // (∀z. (z ∈ X) <=> (z ∈ B1)) <=> (X === B1)))
- val t4 = RightSubstIff(
- t1.bot.left ++ t3.bot.right |- X === B1,
- 2,
- List((X === B1, forall(z, in(z, X) <=> in(z, B1)))),
- LambdaFormulaFormula(Seq(h), h())
- ) // redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)], (∀z. (z ∈ X) <=> (z ∈ B1)) <=> (X === B1))) |- X=B1
- val t5 = Cut(t1.bot.left |- X === B1, 3, 4, t3.bot.right.head) // redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] |- X=B1
- val t6 = Rewrite(Set(H1, G, F) |- forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))) ==> (X === B1), 5) // F |- [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] ==> X=B1
- val i3 = s14.bot // F |- ∀x. (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
- val t7 = RightSubstEq(
- Set(H1, G, F, X === B1) |- forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))),
- -3,
- List((X, B1)),
- LambdaTermFormula(Seq(f), forall(x, in(x, f()) <=> exists(a, in(a, A) /\ phi(x, a))))
- ) // redGoal1 F, X=B1 |- [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
- val t8 = Rewrite(
- Set(H1, G, F) |- X === B1 ==> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))),
- 7
- ) // redGoal1 F |- X=B1 ==> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] -------second half with t6
- val t9 = RightIff(
- Set(H1, G, F) |- (X === B1) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))),
- 6,
- 8,
- X === B1,
- forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))
- ) // goal F |- X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
-
- Proof(steps(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9), imports(i1, i2, i3))
- },
- Vector(13, -3, 14)
- ) // goal F |- X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
- val s16 = RightForall(
- (H1, G, F) |- forall(X, (X === B1) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))),
- 15,
- (X === B1) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))),
- X
- ) // goal F |- ∀X. X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
- val s17 = RightExists(
- (H1, G, F) |- exists(y, forall(X, (X === y) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))))),
- 16,
- forall(X, (X === y) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))),
- y,
- B1
- )
- val s18 = LeftExists((exists(B1, F), G, H1) |- s17.bot.right, 17, F, B1) // ∃B1. F |- ∃B1. ∀X. X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
- val s19 = Rewrite(s18.bot.left |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))), 18) // ∃B1. F |- ∃!X. [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
- val s20 = Cut((G, H1) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))), 7, 19, exists(B1, F))
- val s21 = LeftExists((H1, exists(B, G)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))), 20, G, B)
- val s22 = Cut(H1 |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ phi(x, a)))), 6, 21, exists(B, G))
- val res = steps(s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, s17, s18, s19, s20, s21, s22)
- Proof(res, imports(i1, i2, i3))
- } using (ax"replacementSchema", ax"comprehensionSchema", ax"extensionalityAxiom")
- show
-
- THEOREM("lemmaLayeredTwoArgumentsMap") of
- "∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)" PROOF {
- val a = VariableLabel("a")
- val b = VariableLabel("b")
- val x = VariableLabel("x")
- val x1 = VariableLabel("x1")
- val y = VariableLabel("y")
- val z = VariableLabel("z")
- val a_ = SchematicFunctionLabel("a", 0)
- val b_ = SchematicFunctionLabel("b", 0)
- val x_ = SchematicFunctionLabel("x", 0)
- val x1_ = SchematicFunctionLabel("x1", 0)
- val y_ = SchematicFunctionLabel("y", 0)
- val z_ = SchematicFunctionLabel("z", 0)
- val f = SchematicFunctionLabel("f", 0)
- val h = SchematicPredicateLabel("h", 0)
- val A = SchematicFunctionLabel("A", 0)()
- val X = VariableLabel("X")
- val B = SchematicFunctionLabel("B", 0)()
- val B1 = VariableLabel("B1")
- val phi = SchematicPredicateLabel("phi", 2)
- val psi = SchematicPredicateLabel("psi", 3)
- val H = existsOne(x, phi(x, a))
- val H1 = forall(a, in(a, A) ==> H)
- val i1 = thm"functionalMapping"
- val H2 = instantiatePredicateSchemas(H1, Map(phi -> LambdaTermFormula(Seq(x_, a_), psi(x_, a_, b))))
- val s0 = InstPredSchema((H2) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), -1, Map(phi -> LambdaTermFormula(Seq(x_, a_), psi(x_, a_, b))))
- val s1 = Weakening((H2, in(b, B)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 0)
- val s2 =
- LeftSubstIff((in(b, B) ==> H2, in(b, B)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 1, List((in(b, B), And())), LambdaFormulaFormula(Seq(h), h() ==> H2))
- val s3 = LeftForall((forall(b, in(b, B) ==> H2), in(b, B)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 2, in(b, B) ==> H2, b, b)
- val s4 = Rewrite(forall(b, in(b, B) ==> H2) |- in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 3)
- val s5 = RightForall(
- forall(b, in(b, B) ==> H2) |- forall(b, in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b))))),
- 4,
- in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))),
- b
- )
- val s6 = InstFunSchema(
- forall(b, in(b, B) ==> existsOne(X, phi(X, b))) |- instantiateFunctionSchemas(i1.right.head, Map(SchematicFunctionLabel("A", 0) -> LambdaTermTerm(Nil, B))),
- -1,
- Map(SchematicFunctionLabel("A", 0) -> LambdaTermTerm(Nil, B))
- )
- val s7 = InstPredSchema(
- forall(b, in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b))))) |- existsOne(
- X,
- forall(x, in(x, X) <=> exists(b, in(b, B) /\ forall(x1, in(x1, x) <=> exists(a, in(a, A) /\ psi(x1, a, b)))))
- ),
- 6,
- Map(phi -> LambdaTermFormula(Seq(y_, b_), forall(x, in(x, y_) <=> exists(a, in(a, A) /\ psi(x, a, b_)))))
- )
- val s8 = Cut(
- forall(b, in(b, B) ==> H2) |- existsOne(X, forall(x, in(x, X) <=> exists(b, in(b, B) /\ forall(x1, in(x1, x) <=> exists(a, in(a, A) /\ psi(x1, a, b)))))),
- 5,
- 7,
- forall(b, in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))))
- )
- Proof(Vector(s0, s1, s2, s3, s4, s5, s6, s7, s8), Vector(i1))
- // have ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s0
- // have (b ∈ B), ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s1
- // have (b ∈ B), (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s2
- // have (b ∈ B), ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s3
- // have ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ (b ∈ B) ⇒ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s4
- // have ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∀b. (b ∈ B) ⇒ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s5
- // by thmMapFunctional have ∀b. (b ∈ B) ⇒ ∃!x. ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) phi(x, b) = ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) s6
- // have ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) |- ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) s7
-
- } using (thm"functionalMapping")
- show
-
- THEOREM("applyFunctionToUniqueObject") of
- "∃!x. ?phi(x) ⊢ ∃!z. ∃x. (z = ?F(x)) ∧ ?phi(x)" PROOF {
- val x = VariableLabel("x")
- val x1 = VariableLabel("x1")
- val z = VariableLabel("z")
- val z1 = VariableLabel("z1")
- val F = SchematicFunctionLabel("F", 1)
- val f = SchematicFunctionLabel("f", 0)
- val phi = SchematicPredicateLabel("phi", 1)
- val g = SchematicPredicateLabel("g", 0)
-
- val g2 = SCSubproof({
- val s0 = hypothesis(F(x1) === z)
- val s1 = LeftSubstEq((x === x1, F(x) === z) |- F(x1) === z, 0, List((x, x1)), LambdaTermFormula(Seq(f), F(f()) === z))
- val s2 = LeftSubstIff(Set(phi(x) <=> (x === x1), phi(x), F(x) === z) |- F(x1) === z, 1, List((x === x1, phi(x))), LambdaFormulaFormula(Seq(g), g()))
- val s3 = LeftForall(Set(forall(x, phi(x) <=> (x === x1)), phi(x), F(x) === z) |- F(x1) === z, 2, phi(x) <=> (x === x1), x, x)
- val s4 = Rewrite(Set(forall(x, phi(x) <=> (x === x1)), phi(x) /\ (F(x) === z)) |- F(x1) === z, 3)
- val s5 = LeftExists(Set(forall(x, phi(x) <=> (x === x1)), exists(x, phi(x) /\ (F(x) === z))) |- F(x1) === z, 4, phi(x) /\ (F(x) === z), x)
- val s6 = Rewrite(forall(x, phi(x) <=> (x === x1)) |- exists(x, phi(x) /\ (F(x) === z)) ==> (F(x1) === z), 5)
- Proof(steps(s0, s1, s2, s3, s4, s5, s6))
- }) // redGoal2 ∀x. x=x1 <=> phi(x) ⊢ ∃x. z=F(x) /\ phi(x) ==> F(x1)=z g2.s5
-
- val g1 = SCSubproof({
- val s0 = hypothesis(phi(x1))
- val s1 = LeftForall(forall(x, (x === x1) <=> phi(x)) |- phi(x1), 0, (x === x1) <=> phi(x), x, x1)
- val s2 = hypothesis(z === F(x1))
- val s3 = RightAnd((forall(x, (x === x1) <=> phi(x)), z === F(x1)) |- (z === F(x1)) /\ phi(x1), Seq(2, 1), Seq(z === F(x1), phi(x1)))
- val s4 = RightExists((forall(x, (x === x1) <=> phi(x)), z === F(x1)) |- exists(x, (z === F(x)) /\ phi(x)), 3, (z === F(x)) /\ phi(x), x, x1)
- val s5 = Rewrite(forall(x, (x === x1) <=> phi(x)) |- z === F(x1) ==> exists(x, (z === F(x)) /\ phi(x)), 4)
- Proof(steps(s0, s1, s2, s3, s4, s5))
- })
-
- val s0 = g1
- val s1 = g2
- val s2 = RightIff(forall(x, (x === x1) <=> phi(x)) |- (z === F(x1)) <=> exists(x, (z === F(x)) /\ phi(x)), 0, 1, z === F(x1), exists(x, (z === F(x)) /\ phi(x)))
- val s3 = RightForall(forall(x, (x === x1) <=> phi(x)) |- forall(z, (z === F(x1)) <=> exists(x, (z === F(x)) /\ phi(x))), 2, (z === F(x1)) <=> exists(x, (z === F(x)) /\ phi(x)), z)
- val s4 = RightExists(
- forall(x, (x === x1) <=> phi(x)) |- exists(z1, forall(z, (z === z1) <=> exists(x, (z === F(x)) /\ phi(x)))),
- 3,
- forall(z, (z === z1) <=> exists(x, (z === F(x)) /\ phi(x))),
- z1,
- F(x1)
- )
- val s5 = LeftExists(exists(x1, forall(x, (x === x1) <=> phi(x))) |- exists(z1, forall(z, (z === z1) <=> exists(x, (z === F(x)) /\ phi(x)))), 4, forall(x, (x === x1) <=> phi(x)), x1)
- val s6 = Rewrite(existsOne(x, phi(x)) |- existsOne(z, exists(x, (z === F(x)) /\ phi(x))), 5) // goal ∃!x. phi(x) ⊢ ∃!z. ∃x. z=F(x) /\ phi(x)
- Proof(Vector(s0, s1, s2, s3, s4, s5, s6))
- } using ()
- show
-
- THEOREM("mapTwoArguments") of
- "∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!z. ∃x. (z = U(x)) ∧ ∀x_0. (x_0 ∈ x) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x_0) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)" PROOF {
- val a = VariableLabel("a")
- val b = VariableLabel("b")
- val x = VariableLabel("x")
- val x1 = VariableLabel("x1")
- val x_ = SchematicFunctionLabel("x", 0)
- val y_ = SchematicFunctionLabel("y", 0)
- val F = SchematicFunctionLabel("F", 1)
- val A = SchematicFunctionLabel("A", 0)()
- val B = SchematicFunctionLabel("B", 0)()
- val phi = SchematicPredicateLabel("phi", 1)
- val psi = SchematicPredicateLabel("psi", 3)
-
- val i1 = thm"lemmaLayeredTwoArgumentsMap"
- val i2 = thm"applyFunctionToUniqueObject"
- val rPhi = forall(x, in(x, y_) <=> exists(b, in(b, B) /\ forall(x1, in(x1, x) <=> exists(a, in(a, A) /\ psi(x1, a, b)))))
- val seq0 = instantiatePredicateSchemaInSequent(i2, Map(phi -> LambdaTermFormula(Seq(y_), rPhi)))
- val s0 = InstPredSchema(seq0, -2, Map(phi -> LambdaTermFormula(Seq(y_), rPhi))) // val s0 = InstPredSchema(instantiatePredicateSchemaInSequent(i2, phi, rPhi, Seq(X)), -2, phi, rPhi, Seq(X))
- val seq1 = instantiateFunctionSchemaInSequent(seq0, Map(F -> LambdaTermTerm(Seq(x_), union(x_))))
- val s1 = InstFunSchema(seq1, 0, Map(F -> LambdaTermTerm(Seq(x_), union(x_))))
- val s2 = Cut(i1.left |- seq1.right, -1, 1, seq1.left.head)
- Proof(steps(s0, s1, s2), imports(i1, i2))
- } using (thm"lemmaLayeredTwoArgumentsMap", thm"applyFunctionToUniqueObject")
- show
-
-
-
- val A = SchematicFunctionLabel("A", 0)
- val B = SchematicFunctionLabel("B", 0)
- private val sz = SchematicFunctionLabel("z", 0)
- val cartesianProduct: ConstantFunctionLabel =
- DEFINE("cartProd", A, B) asThe sz suchThat {
- val a = VariableLabel("a")
- val b = VariableLabel("b")
- val x = VariableLabel("x")
- val x0 = VariableLabel("x0")
- val x1 = VariableLabel("x1")
- val A = SchematicFunctionLabel("A", 0)()
- val B = SchematicFunctionLabel("B", 0)()
- exists(x, (sz===union(x)) /\ forall(x0, in(x0, x) <=> exists(b, in(b, B) /\ forall(x1, in(x1, x0) <=> exists(a, in(a, A) /\ (x1 === oPair(a, b)))))))
- } PROOF {
- def makeFunctional(t: Term): Proof = {
- val x = VariableLabel(freshId(t.freeVariables.map(_.id), "x"))
- val y = VariableLabel(freshId(t.freeVariables.map(_.id), "y"))
- val s0 = RightRefl(() |- t === t, t === t)
- val s1 = Rewrite(() |- (x === t) <=> (x === t), 0)
- val s2 = RightForall(() |- forall(x, (x === t) <=> (x === t)), 1, (x === t) <=> (x === t), x)
- val s3 = RightExists(() |- exists(y, forall(x, (x === y) <=> (x === t))), 2, forall(x, (x === y) <=> (x === t)), y, t)
- val s4 = Rewrite(() |- existsOne(x, x === t), 3)
- Proof(s0, s1, s2, s3, s4)
- }
- val a = VariableLabel("a")
- val b = VariableLabel("b")
- val x = VariableLabel("x")
- val a_ = SchematicFunctionLabel("a", 0)
- val b_ = SchematicFunctionLabel("b", 0)
- val x_ = SchematicFunctionLabel("x", 0)
- val x1 = VariableLabel("x1")
- val F = SchematicFunctionLabel("F", 1)
- val A = SchematicFunctionLabel("A", 0)()
- val X = VariableLabel("X")
- val B = SchematicFunctionLabel("B", 0)()
- val phi = SchematicPredicateLabel("phi", 1)
- val psi = SchematicPredicateLabel("psi", 3)
-
- val i1 = thm"mapTwoArguments" // ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!z. ∃x. (z = U(x)) ∧ ∀x_0. (x_0 ∈ x) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x_0) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)
-
- val s0 = SCSubproof({
- val s0 = SCSubproof(makeFunctional(oPair(a, b)))
- val s1 = Weakening((in(b, B), in(a, A)) |- s0.bot.right, 0)
- val s2 = Rewrite(in(b, B) |- in(a, A) ==> s0.bot.right.head, 1)
- val s3 = RightForall(in(b, B) |- forall(a, in(a, A) ==> s0.bot.right.head), 2, in(a, A) ==> s0.bot.right.head, a)
- val s4 = Rewrite(() |- in(b, B) ==> forall(a, in(a, A) ==> s0.bot.right.head), 3)
- val s5 = RightForall(() |- forall(b, in(b, B) ==> forall(a, in(a, A) ==> s0.bot.right.head)), 4, in(b, B) ==> forall(a, in(a, A) ==> s0.bot.right.head), b)
- Proof(steps(s0, s1, s2, s3, s4, s5))
- }) // ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. x= (a, b)
-
- val s1 = InstPredSchema(
- instantiatePredicateSchemaInSequent(i1, Map(psi -> LambdaTermFormula(Seq(x_, a_, b_), x_ === oPair(a_, b_)))),
- -1,
- Map(psi -> LambdaTermFormula(Seq(x_, a_, b_), x_ === oPair(a_, b_)))
- )
- val s2 = Cut(() |- s1.bot.right, 0, 1, s1.bot.left.head)
- Proof(steps(s0, s1, s2), imports(i1))
- } using (thm"mapTwoArguments")
- show
-
-}
diff --git a/src/main/scala/proven/SetTheoryLibrary.scala b/src/main/scala/proven/SetTheoryLibrary.scala
new file mode 100644
index 0000000000000000000000000000000000000000..fd9e5250a1a2bd6ec7ac28ebf4cfd584c46ed590
--- /dev/null
+++ b/src/main/scala/proven/SetTheoryLibrary.scala
@@ -0,0 +1,10 @@
+package proven
+
+/**
+ * Specific implementation of [[utilities.Library]] for Set Theory, with a RunningTheory that is supposed to be used by the standard library.
+ */
+object SetTheoryLibrary extends utilities.Library(lisa.settheory.AxiomaticSetTheory.runningSetTheory) {
+ val AxiomaticSetTheory: lisa.settheory.AxiomaticSetTheory.type = lisa.settheory.AxiomaticSetTheory
+ export AxiomaticSetTheory.*
+
+}
diff --git a/src/main/scala/proven/mathematics/Mapping.scala b/src/main/scala/proven/mathematics/Mapping.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ec6873404f8d4e4b94a4fcc86e7d43956338be57
--- /dev/null
+++ b/src/main/scala/proven/mathematics/Mapping.scala
@@ -0,0 +1,450 @@
+package proven.mathematics
+
+import proven.tactics.Destructors.*
+import proven.tactics.ProofTactics.*
+
+import SetTheory.*
+
+/**
+ * This file contains theorem related to the replacement schema, i.e. how to "map" a set through a functional symbol.
+ * Leads to the definition of the cartesian product.
+ */
+object Mapping extends proven.Main {
+
+ THEOREM("functionalMapping") of
+ "∀a. (a ∈ ?A) ⇒ ∃!x. ?phi(x, a) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ ?A) ∧ ?phi(x, a)" PROOF {
+ val a = VariableLabel("a")
+ val b = VariableLabel("b")
+ val x = VariableLabel("x")
+ val y = VariableLabel("y")
+ val z = VariableLabel("z")
+ val a1 = SchematicFunctionLabel("a", 0)
+ val b1 = SchematicFunctionLabel("b", 0)
+ val x1 = SchematicFunctionLabel("x", 0)
+ val y1 = SchematicFunctionLabel("y", 0)
+ val z1 = SchematicFunctionLabel("z", 0)
+ val f = SchematicFunctionLabel("f", 0)
+ val h = SchematicPredicateLabel("h", 0)
+ val A = SchematicFunctionLabel("A", 0)()
+ val X = VariableLabel("X")
+ val B = VariableLabel("B")
+ val B1 = VariableLabel("B1")
+ val phi = SchematicPredicateLabel("phi", 2)
+ val sPhi = SchematicPredicateLabel("P", 2)
+ val sPsi = SchematicPredicateLabel("P", 3)
+
+ val H = existsOne(x, phi(x, a))
+ val H1 = forall(a, in(a, A) ==> H)
+ val s0 = hypothesis(H) // () |- existsOne(x, phi(x, a)))
+ val s1 = Weakening((H, in(a, A)) |- existsOne(x, phi(x, a)), 0)
+ val s2 = Rewrite((H) |- in(a, A) ==> existsOne(x, phi(x, a)), 1)
+ // val s3 = RightForall((H) |- forall(a, in(a, A) ==> existsOne(x, phi(x, a))), 2, in(a, A) ==> existsOne(x, phi(x, a)), a) // () |- ∀a∈A. ∃!x. phi(x, a)
+ val s3 = hypothesis(H1)
+ val i1 = () |- replacementSchema
+ val p0 = InstPredSchema(
+ () |- instantiatePredicateSchemas(replacementSchema, Map(sPsi -> LambdaTermFormula(Seq(y1, a1, x1), phi(x1, a1)))),
+ -1,
+ Map(sPsi -> LambdaTermFormula(Seq(y1, a1, x1), phi(x1, a1)))
+ )
+ val p1 = instantiateForall(Proof(steps(p0), imports(i1)), A)
+ val s4 = SCSubproof(p1, Seq(-1)) //
+ val s5 = Rewrite(s3.bot.right.head |- exists(B, forall(x, in(x, A) ==> exists(y, in(y, B) /\ (phi(y, x))))), 4)
+ val s6 = Cut((H1) |- exists(B, forall(x, in(x, A) ==> exists(y, in(y, B) /\ (phi(y, x))))), 3, 5, s3.bot.right.head) // ⊢ ∃B. ∀x. (x ∈ A) ⇒ ∃y. (y ∈ B) ∧ (y = (x, b))
+
+ val i2 = () |- comprehensionSchema // forall(z, exists(y, forall(x, in(x,y) <=> (in(x,z) /\ sPhi(x,z)))))
+ val q0 = InstPredSchema(
+ () |- instantiatePredicateSchemas(comprehensionSchema, Map(sPhi -> LambdaTermFormula(Seq(x1, z1), exists(a, in(a, A) /\ phi(x1, a))))),
+ -1,
+ Map(sPhi -> LambdaTermFormula(Seq(x1, z1), exists(a, in(a, A) /\ phi(x1, a))))
+ )
+ val q1 = instantiateForall(Proof(steps(q0), imports(i2)), B)
+ val s7 = SCSubproof(q1, Seq(-2)) // ∃y. ∀x. (x ∈ y) ↔ (x ∈ B) ∧ ∃a. a ∈ A /\ x = (a, b) := exists(y, F(y) )
+ Proof(steps(s0, s1, s2, s3, s4, s5, s6, s7), imports(i1, i2))
+ val s8 = SCSubproof({
+ val y1 = VariableLabel("y1")
+ val f = SchematicFunctionLabel("f", 0)
+ val s0 = hypothesis(in(y1, B))
+ val s1 = RightSubstEq((in(y1, B), x === y1) |- in(x, B), 0, List((x, y1)), LambdaTermFormula(Seq(f), in(f(), B)))
+ val s2 = LeftSubstIff(Set(in(y1, B), (x === y1) <=> phi(x, a), phi(x, a)) |- in(x, B), 1, List(((x === y1), phi(x, a))), LambdaFormulaFormula(Seq(h), h()))
+ val s3 = LeftSubstEq(Set(y === y1, in(y1, B), (x === y) <=> phi(x, a), phi(x, a)) |- in(x, B), 2, List((y, y1)), LambdaTermFormula(Seq(f), (x === f()) <=> phi(x, a)))
+ val s4 = LeftSubstIff(Set((y === y1) <=> phi(y1, a), phi(y1, a), in(y1, B), (x === y) <=> phi(x, a), phi(x, a)) |- in(x, B), 3, List((phi(y1, a), y1 === y)), LambdaFormulaFormula(Seq(h), h()))
+ val s5 = LeftForall(Set(forall(x, (y === x) <=> phi(x, a)), phi(y1, a), in(y1, B), (x === y) <=> phi(x, a), phi(x, a)) |- in(x, B), 4, (y === x) <=> phi(x, a), x, y1)
+ val s6 = LeftForall(Set(forall(x, (y === x) <=> phi(x, a)), phi(y1, a), in(y1, B), phi(x, a)) |- in(x, B), 5, (x === y) <=> phi(x, a), x, x)
+ val s7 = LeftExists(Set(exists(y, forall(x, (y === x) <=> phi(x, a))), phi(y1, a), in(y1, B), phi(x, a)) |- in(x, B), 6, forall(x, (y === x) <=> phi(x, a)), y)
+ val s8 = Rewrite(Set(exists(y, forall(x, (y === x) <=> phi(x, a))), phi(y1, a) /\ in(y1, B), phi(x, a)) |- in(x, B), 7)
+ val s9 = LeftExists(Set(exists(y, forall(x, (y === x) <=> phi(x, a))), exists(y1, phi(y1, a) /\ in(y1, B)), phi(x, a)) |- in(x, B), 8, phi(y1, a) /\ in(y1, B), y1)
+ val s10 = Rewrite(Set(exists(y, forall(x, (y === x) <=> phi(x, a))), And() ==> exists(y, phi(y, a) /\ in(y, B)), phi(x, a)) |- in(x, B), 9)
+ val s11 = LeftSubstIff(
+ Set(exists(y, forall(x, (y === x) <=> phi(x, a))), in(a, A) ==> exists(y, phi(y, a) /\ in(y, B)), phi(x, a), in(a, A)) |- in(x, B),
+ 10,
+ List((And(), in(a, A))),
+ LambdaFormulaFormula(Seq(h), h() ==> exists(y, phi(y, a) /\ in(y, B)))
+ )
+ val s12 = LeftForall(
+ Set(exists(y, forall(x, (y === x) <=> phi(x, a))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a), in(a, A)) |- in(x, B),
+ 11,
+ in(a, A) ==> exists(y, phi(y, a) /\ in(y, B)),
+ a,
+ a
+ )
+ val s13 = LeftSubstIff(
+ Set(in(a, A) ==> exists(y, forall(x, (y === x) <=> phi(x, a))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a), in(a, A)) |- in(x, B),
+ 12,
+ List((And(), in(a, A))),
+ LambdaFormulaFormula(Seq(h), h() ==> exists(y, forall(x, (y === x) <=> phi(x, a))))
+ )
+ val s14 = LeftForall(
+ Set(forall(a, in(a, A) ==> exists(y, forall(x, (y === x) <=> phi(x, a)))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a), in(a, A)) |- in(x, B),
+ 13,
+ in(a, A) ==> exists(y, forall(x, (y === x) <=> phi(x, a))),
+ a,
+ a
+ )
+ val s15 = Rewrite(Set(forall(a, in(a, A) ==> exists(y, forall(x, (y === x) <=> phi(x, a)))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a) /\ in(a, A)) |- in(x, B), 14)
+ val s16 = LeftExists(
+ Set(forall(a, in(a, A) ==> exists(y, forall(x, (y === x) <=> phi(x, a)))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), exists(a, phi(x, a) /\ in(a, A))) |- in(x, B),
+ 15,
+ phi(x, a) /\ in(a, A),
+ a
+ )
+ val truc = forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B)))
+ val s17 = Rewrite(Set(forall(a, in(a, A) ==> existsOne(x, phi(x, a))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), exists(a, phi(x, a) /\ in(a, A))) |- in(x, B), 16)
+ Proof(steps(s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, s17))
+ // goal H, ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B)
+ // redGoal ∀a.(a ∈ A) => ∃!x. phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B) s17
+ // redGoal ∀a.(a ∈ A) => ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B) s16
+ // redGoal ∀a.(a ∈ A) => ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A ∧ phi(x, a) |- (x ∈ B) s15
+ // redGoal ∀a.(a ∈ A) => ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A, phi(x, a) |- (x ∈ B) s14
+ // redGoal (a ∈ A) => ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A, phi(x, a) |- (x ∈ B) s13
+ // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A, phi(x, a) |- (x ∈ B) s12
+ // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A, phi(x, a) |- (x ∈ B) s11
+ // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A <=> T, phi(x, a) |- (x ∈ B) s11
+ // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), T ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A <=> T, phi(x, a) |- (x ∈ B) s10
+ // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), ∃y1. y1 ∈ B ∧ phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s9
+ // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), y1 ∈ B ∧ phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s8
+ // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), y1 ∈ B, phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s7
+ // redGoal ∀x. (x=y) ↔ phi(x, a), y1 ∈ B, phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s6
+ // redGoal (x=y) ↔ phi(x, a), ∀x. (x=y) ↔ phi(x, a), y1 ∈ B, phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s5
+ // redGoal (x=y) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s4
+ // redGoal (x=y) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, (y1=y), a ∈ A, phi(x, a) |- (x ∈ B) s3
+ // redGoal (x=y1) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, (y1=y), a ∈ A, phi(x, a) |- (x ∈ B) s2
+ // redGoal (x=y1) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, (y1=y), a ∈ A, x=y1 |- (x ∈ B) s1
+ // redGoal (x=y1) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, (y1=y), a ∈ A, x=y1 |- (y1 ∈ B) s0
+
+ }) // H, ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B)
+
+ val G = forall(a, in(a, A) ==> exists(y, in(y, B) /\ (phi(y, a))))
+ val F = forall(x, iff(in(x, B1), in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a)))))
+ val s9 = SCSubproof({
+ val p0 = instantiateForall(Proof(hypothesis(F)), x)
+ val left = in(x, B1)
+ val right = in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a)))
+ val p1 = p0.withNewSteps(Vector(Rewrite(F |- (left ==> right) /\ (right ==> left), p0.length - 1)))
+ val p2 = destructRightAnd(p1, (right ==> left), (left ==> right)) // F |- in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a))) => in(x, B1)
+ val p3 = p2.withNewSteps(Vector(Rewrite(Set(F, in(x, B), exists(a, in(a, A) /\ (phi(x, a)))) |- in(x, B1), p2.length - 1)))
+ p3
+ }) // have F, (x ∈ B), ∃a. a ∈ A ∧ x = (a, b) |- (x ∈ B1)
+ val s10 = Cut(Set(F, G, H1, exists(a, in(a, A) /\ (phi(x, a)))) |- in(x, B1), 8, 9, in(x, B)) // redGoal F, ∃a. a ∈ A ∧ x = (a, b), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ y = (a, b) |- (x ∈ B1)
+ val s11 = Rewrite(Set(H1, G, F) |- exists(a, in(a, A) /\ (phi(x, a))) ==> in(x, B1), 10) // F |- ∃a. a ∈ A ∧ x = (a, b) => (x ∈ B1) --- half
+ val s12 = SCSubproof({
+ val p0 = instantiateForall(Proof(hypothesis(F)), x)
+ val left = in(x, B1)
+ val right = in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a)))
+ val p1 = p0.withNewSteps(Vector(Rewrite(F |- (left ==> right) /\ (right ==> left), p0.length - 1)))
+ val p2 = destructRightAnd(p1, (left ==> right), (right ==> left)) // F |- in(x, B1) => in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a))) =>
+ val p3 = p2.withNewSteps(Vector(Rewrite(Set(F, in(x, B1)) |- exists(a, in(a, A) /\ (phi(x, a))) /\ in(x, B), p2.length - 1)))
+ val p4 = destructRightAnd(p3, exists(a, in(a, A) /\ (phi(x, a))), in(x, B))
+ val p5 = p4.withNewSteps(Vector(Rewrite(F |- in(x, B1) ==> exists(a, in(a, A) /\ (phi(x, a))), p4.length - 1)))
+ p5
+ }) // have F |- (x ∈ B1) ⇒ ∃a. a ∈ A ∧ x = (a, b) --- other half
+ val s13 = RightIff((H1, G, F) |- in(x, B1) <=> exists(a, in(a, A) /\ (phi(x, a))), 11, 12, in(x, B1), exists(a, in(a, A) /\ (phi(x, a)))) // have F |- (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
+ val s14 =
+ RightForall(
+ (H1, G, F) |- forall(x, in(x, B1) <=> exists(a, in(a, A) /\ (phi(x, a)))),
+ 13,
+ in(x, B1) <=> exists(a, in(a, A) /\ (phi(x, a))),
+ x
+ ) // G, F |- ∀x. (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
+
+ val i3 = () |- extensionalityAxiom
+ val s15 = SCSubproof(
+ {
+ val i1 = s13.bot // G, F |- (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
+ val i2 = () |- extensionalityAxiom
+ val t0 = RightSubstIff(
+ Set(H1, G, F, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))) |- in(x, X) <=> in(x, B1),
+ -1,
+ List((in(x, X), exists(a, in(a, A) /\ (phi(x, a))))),
+ LambdaFormulaFormula(Seq(h), h() <=> in(x, B1))
+ ) // redGoal2 F, (z ∈ X) <=> ∃a. a ∈ A ∧ z = (a, b) |- (z ∈ X) <=> (z ∈ B1)
+ val t1 = LeftForall(
+ Set(H1, G, F, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))) |- in(x, X) <=> in(x, B1),
+ 0,
+ in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))),
+ x,
+ x
+ ) // redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] |- (z ∈ X) <=> (z ∈ B1)
+ val t2 = RightForall(t1.bot.left |- forall(x, in(x, X) <=> in(x, B1)), 1, in(x, X) <=> in(x, B1), x) // redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] |- ∀z. (z ∈ X) <=> (z ∈ B1)
+ val t3 =
+ SCSubproof(instantiateForall(Proof(steps(Rewrite(() |- extensionalityAxiom, -1)), imports(() |- extensionalityAxiom)), X, B1), Vector(-2)) // (∀z. (z ∈ X) <=> (z ∈ B1)) <=> (X === B1)))
+ val t4 = RightSubstIff(
+ t1.bot.left ++ t3.bot.right |- X === B1,
+ 2,
+ List((X === B1, forall(z, in(z, X) <=> in(z, B1)))),
+ LambdaFormulaFormula(Seq(h), h())
+ ) // redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)], (∀z. (z ∈ X) <=> (z ∈ B1)) <=> (X === B1))) |- X=B1
+ val t5 = Cut(t1.bot.left |- X === B1, 3, 4, t3.bot.right.head) // redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] |- X=B1
+ val t6 = Rewrite(Set(H1, G, F) |- forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))) ==> (X === B1), 5) // F |- [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] ==> X=B1
+ val i3 = s14.bot // F |- ∀x. (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
+ val t7 = RightSubstEq(
+ Set(H1, G, F, X === B1) |- forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))),
+ -3,
+ List((X, B1)),
+ LambdaTermFormula(Seq(f), forall(x, in(x, f()) <=> exists(a, in(a, A) /\ phi(x, a))))
+ ) // redGoal1 F, X=B1 |- [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
+ val t8 = Rewrite(
+ Set(H1, G, F) |- X === B1 ==> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))),
+ 7
+ ) // redGoal1 F |- X=B1 ==> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] -------second half with t6
+ val t9 = RightIff(
+ Set(H1, G, F) |- (X === B1) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))),
+ 6,
+ 8,
+ X === B1,
+ forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))
+ ) // goal F |- X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
+
+ Proof(steps(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9), imports(i1, i2, i3))
+ },
+ Vector(13, -3, 14)
+ ) // goal F |- X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
+ val s16 = RightForall(
+ (H1, G, F) |- forall(X, (X === B1) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))),
+ 15,
+ (X === B1) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))),
+ X
+ ) // goal F |- ∀X. X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
+ val s17 = RightExists(
+ (H1, G, F) |- exists(y, forall(X, (X === y) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))))),
+ 16,
+ forall(X, (X === y) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))),
+ y,
+ B1
+ )
+ val s18 = LeftExists((exists(B1, F), G, H1) |- s17.bot.right, 17, F, B1) // ∃B1. F |- ∃B1. ∀X. X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
+ val s19 = Rewrite(s18.bot.left |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))), 18) // ∃B1. F |- ∃!X. [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
+ val s20 = Cut((G, H1) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))), 7, 19, exists(B1, F))
+ val s21 = LeftExists((H1, exists(B, G)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))), 20, G, B)
+ val s22 = Cut(H1 |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ phi(x, a)))), 6, 21, exists(B, G))
+ val res = steps(s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, s17, s18, s19, s20, s21, s22)
+ Proof(res, imports(i1, i2, i3))
+ } using (ax"replacementSchema", ax"comprehensionSchema", ax"extensionalityAxiom")
+ show
+
+ THEOREM("lemmaLayeredTwoArgumentsMap") of
+ "∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)" PROOF {
+ val a = VariableLabel("a")
+ val b = VariableLabel("b")
+ val x = VariableLabel("x")
+ val x1 = VariableLabel("x1")
+ val y = VariableLabel("y")
+ val z = VariableLabel("z")
+ val a_ = SchematicFunctionLabel("a", 0)
+ val b_ = SchematicFunctionLabel("b", 0)
+ val x_ = SchematicFunctionLabel("x", 0)
+ val x1_ = SchematicFunctionLabel("x1", 0)
+ val y_ = SchematicFunctionLabel("y", 0)
+ val z_ = SchematicFunctionLabel("z", 0)
+ val f = SchematicFunctionLabel("f", 0)
+ val h = SchematicPredicateLabel("h", 0)
+ val A = SchematicFunctionLabel("A", 0)()
+ val X = VariableLabel("X")
+ val B = SchematicFunctionLabel("B", 0)()
+ val B1 = VariableLabel("B1")
+ val phi = SchematicPredicateLabel("phi", 2)
+ val psi = SchematicPredicateLabel("psi", 3)
+ val H = existsOne(x, phi(x, a))
+ val H1 = forall(a, in(a, A) ==> H)
+ val i1 = thm"functionalMapping"
+ val H2 = instantiatePredicateSchemas(H1, Map(phi -> LambdaTermFormula(Seq(x_, a_), psi(x_, a_, b))))
+ val s0 = InstPredSchema((H2) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), -1, Map(phi -> LambdaTermFormula(Seq(x_, a_), psi(x_, a_, b))))
+ val s1 = Weakening((H2, in(b, B)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 0)
+ val s2 =
+ LeftSubstIff((in(b, B) ==> H2, in(b, B)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 1, List((in(b, B), And())), LambdaFormulaFormula(Seq(h), h() ==> H2))
+ val s3 = LeftForall((forall(b, in(b, B) ==> H2), in(b, B)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 2, in(b, B) ==> H2, b, b)
+ val s4 = Rewrite(forall(b, in(b, B) ==> H2) |- in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 3)
+ val s5 = RightForall(
+ forall(b, in(b, B) ==> H2) |- forall(b, in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b))))),
+ 4,
+ in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))),
+ b
+ )
+ val s6 = InstFunSchema(
+ forall(b, in(b, B) ==> existsOne(X, phi(X, b))) |- instantiateFunctionSchemas(i1.right.head, Map(SchematicFunctionLabel("A", 0) -> LambdaTermTerm(Nil, B))),
+ -1,
+ Map(SchematicFunctionLabel("A", 0) -> LambdaTermTerm(Nil, B))
+ )
+ val s7 = InstPredSchema(
+ forall(b, in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b))))) |- existsOne(
+ X,
+ forall(x, in(x, X) <=> exists(b, in(b, B) /\ forall(x1, in(x1, x) <=> exists(a, in(a, A) /\ psi(x1, a, b)))))
+ ),
+ 6,
+ Map(phi -> LambdaTermFormula(Seq(y_, b_), forall(x, in(x, y_) <=> exists(a, in(a, A) /\ psi(x, a, b_)))))
+ )
+ val s8 = Cut(
+ forall(b, in(b, B) ==> H2) |- existsOne(X, forall(x, in(x, X) <=> exists(b, in(b, B) /\ forall(x1, in(x1, x) <=> exists(a, in(a, A) /\ psi(x1, a, b)))))),
+ 5,
+ 7,
+ forall(b, in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))))
+ )
+ Proof(Vector(s0, s1, s2, s3, s4, s5, s6, s7, s8), Vector(i1))
+ // have ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s0
+ // have (b ∈ B), ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s1
+ // have (b ∈ B), (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s2
+ // have (b ∈ B), ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s3
+ // have ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ (b ∈ B) ⇒ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s4
+ // have ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∀b. (b ∈ B) ⇒ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s5
+ // by thmMapFunctional have ∀b. (b ∈ B) ⇒ ∃!x. ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) phi(x, b) = ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) s6
+ // have ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) |- ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) s7
+
+ } using (thm"functionalMapping")
+ show
+
+ THEOREM("applyFunctionToUniqueObject") of
+ "∃!x. ?phi(x) ⊢ ∃!z. ∃x. (z = ?F(x)) ∧ ?phi(x)" PROOF {
+ val x = VariableLabel("x")
+ val x1 = VariableLabel("x1")
+ val z = VariableLabel("z")
+ val z1 = VariableLabel("z1")
+ val F = SchematicFunctionLabel("F", 1)
+ val f = SchematicFunctionLabel("f", 0)
+ val phi = SchematicPredicateLabel("phi", 1)
+ val g = SchematicPredicateLabel("g", 0)
+
+ val g2 = SCSubproof({
+ val s0 = hypothesis(F(x1) === z)
+ val s1 = LeftSubstEq((x === x1, F(x) === z) |- F(x1) === z, 0, List((x, x1)), LambdaTermFormula(Seq(f), F(f()) === z))
+ val s2 = LeftSubstIff(Set(phi(x) <=> (x === x1), phi(x), F(x) === z) |- F(x1) === z, 1, List((x === x1, phi(x))), LambdaFormulaFormula(Seq(g), g()))
+ val s3 = LeftForall(Set(forall(x, phi(x) <=> (x === x1)), phi(x), F(x) === z) |- F(x1) === z, 2, phi(x) <=> (x === x1), x, x)
+ val s4 = Rewrite(Set(forall(x, phi(x) <=> (x === x1)), phi(x) /\ (F(x) === z)) |- F(x1) === z, 3)
+ val s5 = LeftExists(Set(forall(x, phi(x) <=> (x === x1)), exists(x, phi(x) /\ (F(x) === z))) |- F(x1) === z, 4, phi(x) /\ (F(x) === z), x)
+ val s6 = Rewrite(forall(x, phi(x) <=> (x === x1)) |- exists(x, phi(x) /\ (F(x) === z)) ==> (F(x1) === z), 5)
+ Proof(steps(s0, s1, s2, s3, s4, s5, s6))
+ }) // redGoal2 ∀x. x=x1 <=> phi(x) ⊢ ∃x. z=F(x) /\ phi(x) ==> F(x1)=z g2.s5
+
+ val g1 = SCSubproof({
+ val s0 = hypothesis(phi(x1))
+ val s1 = LeftForall(forall(x, (x === x1) <=> phi(x)) |- phi(x1), 0, (x === x1) <=> phi(x), x, x1)
+ val s2 = hypothesis(z === F(x1))
+ val s3 = RightAnd((forall(x, (x === x1) <=> phi(x)), z === F(x1)) |- (z === F(x1)) /\ phi(x1), Seq(2, 1), Seq(z === F(x1), phi(x1)))
+ val s4 = RightExists((forall(x, (x === x1) <=> phi(x)), z === F(x1)) |- exists(x, (z === F(x)) /\ phi(x)), 3, (z === F(x)) /\ phi(x), x, x1)
+ val s5 = Rewrite(forall(x, (x === x1) <=> phi(x)) |- z === F(x1) ==> exists(x, (z === F(x)) /\ phi(x)), 4)
+ Proof(steps(s0, s1, s2, s3, s4, s5))
+ })
+
+ val s0 = g1
+ val s1 = g2
+ val s2 = RightIff(forall(x, (x === x1) <=> phi(x)) |- (z === F(x1)) <=> exists(x, (z === F(x)) /\ phi(x)), 0, 1, z === F(x1), exists(x, (z === F(x)) /\ phi(x)))
+ val s3 = RightForall(forall(x, (x === x1) <=> phi(x)) |- forall(z, (z === F(x1)) <=> exists(x, (z === F(x)) /\ phi(x))), 2, (z === F(x1)) <=> exists(x, (z === F(x)) /\ phi(x)), z)
+ val s4 = RightExists(
+ forall(x, (x === x1) <=> phi(x)) |- exists(z1, forall(z, (z === z1) <=> exists(x, (z === F(x)) /\ phi(x)))),
+ 3,
+ forall(z, (z === z1) <=> exists(x, (z === F(x)) /\ phi(x))),
+ z1,
+ F(x1)
+ )
+ val s5 = LeftExists(exists(x1, forall(x, (x === x1) <=> phi(x))) |- exists(z1, forall(z, (z === z1) <=> exists(x, (z === F(x)) /\ phi(x)))), 4, forall(x, (x === x1) <=> phi(x)), x1)
+ val s6 = Rewrite(existsOne(x, phi(x)) |- existsOne(z, exists(x, (z === F(x)) /\ phi(x))), 5) // goal ∃!x. phi(x) ⊢ ∃!z. ∃x. z=F(x) /\ phi(x)
+ Proof(Vector(s0, s1, s2, s3, s4, s5, s6))
+ } using ()
+ show
+
+ THEOREM("mapTwoArguments") of
+ "∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!z. ∃x. (z = U(x)) ∧ ∀x_0. (x_0 ∈ x) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x_0) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)" PROOF {
+ val a = VariableLabel("a")
+ val b = VariableLabel("b")
+ val x = VariableLabel("x")
+ val x1 = VariableLabel("x1")
+ val x_ = SchematicFunctionLabel("x", 0)
+ val y_ = SchematicFunctionLabel("y", 0)
+ val F = SchematicFunctionLabel("F", 1)
+ val A = SchematicFunctionLabel("A", 0)()
+ val B = SchematicFunctionLabel("B", 0)()
+ val phi = SchematicPredicateLabel("phi", 1)
+ val psi = SchematicPredicateLabel("psi", 3)
+
+ val i1 = thm"lemmaLayeredTwoArgumentsMap"
+ val i2 = thm"applyFunctionToUniqueObject"
+ val rPhi = forall(x, in(x, y_) <=> exists(b, in(b, B) /\ forall(x1, in(x1, x) <=> exists(a, in(a, A) /\ psi(x1, a, b)))))
+ val seq0 = instantiatePredicateSchemaInSequent(i2, Map(phi -> LambdaTermFormula(Seq(y_), rPhi)))
+ val s0 = InstPredSchema(seq0, -2, Map(phi -> LambdaTermFormula(Seq(y_), rPhi))) // val s0 = InstPredSchema(instantiatePredicateSchemaInSequent(i2, phi, rPhi, Seq(X)), -2, phi, rPhi, Seq(X))
+ val seq1 = instantiateFunctionSchemaInSequent(seq0, Map(F -> LambdaTermTerm(Seq(x_), union(x_))))
+ val s1 = InstFunSchema(seq1, 0, Map(F -> LambdaTermTerm(Seq(x_), union(x_))))
+ val s2 = Cut(i1.left |- seq1.right, -1, 1, seq1.left.head)
+ Proof(steps(s0, s1, s2), imports(i1, i2))
+ } using (thm"lemmaLayeredTwoArgumentsMap", thm"applyFunctionToUniqueObject")
+ show
+
+ val A = SchematicFunctionLabel("A", 0)
+ val B = SchematicFunctionLabel("B", 0)
+ private val sz = SchematicFunctionLabel("z", 0)
+ val cartesianProduct: ConstantFunctionLabel =
+ DEFINE("cartProd", A, B) asThe sz suchThat {
+ val a = VariableLabel("a")
+ val b = VariableLabel("b")
+ val x = VariableLabel("x")
+ val x0 = VariableLabel("x0")
+ val x1 = VariableLabel("x1")
+ val A = SchematicFunctionLabel("A", 0)()
+ val B = SchematicFunctionLabel("B", 0)()
+ exists(x, (sz === union(x)) /\ forall(x0, in(x0, x) <=> exists(b, in(b, B) /\ forall(x1, in(x1, x0) <=> exists(a, in(a, A) /\ (x1 === oPair(a, b)))))))
+ } PROOF {
+ def makeFunctional(t: Term): Proof = {
+ val x = VariableLabel(freshId(t.freeVariables.map(_.id), "x"))
+ val y = VariableLabel(freshId(t.freeVariables.map(_.id), "y"))
+ val s0 = RightRefl(() |- t === t, t === t)
+ val s1 = Rewrite(() |- (x === t) <=> (x === t), 0)
+ val s2 = RightForall(() |- forall(x, (x === t) <=> (x === t)), 1, (x === t) <=> (x === t), x)
+ val s3 = RightExists(() |- exists(y, forall(x, (x === y) <=> (x === t))), 2, forall(x, (x === y) <=> (x === t)), y, t)
+ val s4 = Rewrite(() |- existsOne(x, x === t), 3)
+ Proof(s0, s1, s2, s3, s4)
+ }
+
+ val a = VariableLabel("a")
+ val b = VariableLabel("b")
+ val x = VariableLabel("x")
+ val a_ = SchematicFunctionLabel("a", 0)
+ val b_ = SchematicFunctionLabel("b", 0)
+ val x_ = SchematicFunctionLabel("x", 0)
+ val x1 = VariableLabel("x1")
+ val F = SchematicFunctionLabel("F", 1)
+ val A = SchematicFunctionLabel("A", 0)()
+ val X = VariableLabel("X")
+ val B = SchematicFunctionLabel("B", 0)()
+ val phi = SchematicPredicateLabel("phi", 1)
+ val psi = SchematicPredicateLabel("psi", 3)
+
+ val i1 = thm"mapTwoArguments" // ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!z. ∃x. (z = U(x)) ∧ ∀x_0. (x_0 ∈ x) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x_0) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)
+
+ val s0 = SCSubproof({
+ val s0 = SCSubproof(makeFunctional(oPair(a, b)))
+ val s1 = Weakening((in(b, B), in(a, A)) |- s0.bot.right, 0)
+ val s2 = Rewrite(in(b, B) |- in(a, A) ==> s0.bot.right.head, 1)
+ val s3 = RightForall(in(b, B) |- forall(a, in(a, A) ==> s0.bot.right.head), 2, in(a, A) ==> s0.bot.right.head, a)
+ val s4 = Rewrite(() |- in(b, B) ==> forall(a, in(a, A) ==> s0.bot.right.head), 3)
+ val s5 = RightForall(() |- forall(b, in(b, B) ==> forall(a, in(a, A) ==> s0.bot.right.head)), 4, in(b, B) ==> forall(a, in(a, A) ==> s0.bot.right.head), b)
+ Proof(steps(s0, s1, s2, s3, s4, s5))
+ }) // ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. x= (a, b)
+
+ val s1 = InstPredSchema(
+ instantiatePredicateSchemaInSequent(i1, Map(psi -> LambdaTermFormula(Seq(x_, a_, b_), x_ === oPair(a_, b_)))),
+ -1,
+ Map(psi -> LambdaTermFormula(Seq(x_, a_, b_), x_ === oPair(a_, b_)))
+ )
+ val s2 = Cut(() |- s1.bot.right, 0, 1, s1.bot.left.head)
+ Proof(steps(s0, s1, s2), imports(i1))
+ } using (thm"mapTwoArguments")
+ show
+
+}
diff --git a/src/main/scala/proven/mathematics/SetTheory.scala b/src/main/scala/proven/mathematics/SetTheory.scala
new file mode 100644
index 0000000000000000000000000000000000000000..add21cfebf996abea27b41f6b3730d6e347d7cfd
--- /dev/null
+++ b/src/main/scala/proven/mathematics/SetTheory.scala
@@ -0,0 +1,369 @@
+package proven.mathematics
+
+import proven.tactics.Destructors.*
+import proven.tactics.ProofTactics.*
+
+/**
+ * An embryo of mathematical development, containing a few example theorems and the definition of the ordered pair.
+ */
+object SetTheory extends proven.Main {
+
+ THEOREM("russelParadox") of "∀x. (x ∈ ?y) ↔ ¬(x ∈ x) ⊢" PROOF {
+ val y = SchematicFunctionLabel("y", 0)
+ val x_ = VariableLabel("x")
+ val contra = in(y, y) <=> !in(y, y)
+ val s0 = Hypothesis(contra |- contra, contra)
+ val s1 = LeftForall(forall(x_, in(x_, y) <=> !in(x_, x_)) |- contra, 0, in(x_, y) <=> !in(x_, x_), x_, y)
+ val s2 = Rewrite(forall(x_, in(x_, y) <=> !in(x_, x_)) |- (), 1)
+ Proof(s0, s1, s2)
+ } using ()
+ thm"russelParadox".show
+
+ THEOREM("unorderedPair_symmetry") of
+ "⊢ ∀y, x. {x, y} = {y, x}" PROOF {
+ val x = VariableLabel("x")
+ val y = VariableLabel("y")
+ val z = VariableLabel("z")
+ val h = SchematicPredicateLabel("h", 0)
+ val fin = SCSubproof(
+ {
+ val pr0 = SCSubproof(
+ {
+ val pairSame11 = instantiateForall(new Proof(steps(), imports(ax"pairAxiom")), pairAxiom, x)
+ val pairSame12 = instantiateForall(pairSame11, pairSame11.conclusion.right.head, y)
+ instantiateForall(pairSame12, pairSame12.conclusion.right.head, z)
+ },
+ Seq(-1)
+ )
+ val pr1 = SCSubproof(
+ {
+ val pairSame21 = instantiateForall(new Proof(steps(), imports(ax"pairAxiom")), pairAxiom, y)
+ val pairSame22 = instantiateForall(pairSame21, pairSame21.conclusion.right.head, x)
+ instantiateForall(pairSame22, pairSame22.conclusion.right.head, z)
+ },
+ Seq(-1)
+ )
+ val pr2 = RightSubstIff(
+ Sequent(pr1.bot.right, Set(in(z, pair(x, y)) <=> in(z, pair(y, x)))),
+ 0,
+ List(((x === z) \/ (y === z), in(z, pair(y, x)))),
+ LambdaFormulaFormula(Seq(h), in(z, pair(x, y)) <=> h())
+ )
+ val pr3 = Cut(Sequent(pr1.bot.left, pr2.bot.right), 1, 2, pr2.bot.left.head)
+ val pr4 = RightForall(Sequent(Set(), Set(forall(z, pr2.bot.right.head))), 3, pr2.bot.right.head, z)
+ Proof(steps(pr0, pr1, pr2, pr3, pr4), imports(ax"pairAxiom"))
+ },
+ Seq(-2)
+ )
+ val pairExt = SCSubproof(
+ {
+ val pairExt1 = instantiateForall(Proof(steps(), imports(ax"extensionalityAxiom")), ax"extensionalityAxiom", pair(x, y))
+ instantiateForall(pairExt1, pairExt1.conclusion.right.head, pair(y, x))
+ },
+ Seq(-1)
+ )
+ val fin2 = byEquiv(
+ pairExt.bot.right.head,
+ fin.bot.right.head
+ )(pairExt, fin)
+ val fin3 = generalizeToForall(fin2, fin2.conclusion.right.head, x)
+ val fin4 = generalizeToForall(fin3, fin3.conclusion.right.head, y)
+ fin4.copy(imports = imports(ax"extensionalityAxiom", ax"pairAxiom"))
+ } using (ax"extensionalityAxiom", AxiomaticSetTheory.pairAxiom)
+ show
+
+ // This proof is old and very unoptimised
+ THEOREM("unorderedPair_deconstruction") of
+ "⊢ ∀x, y, x', y'. ({x, y} = {x', y'}) ⇒ (y' = y) ∧ (x' = x) ∨ (x = y') ∧ (y = x')" PROOF {
+ val x = VariableLabel("x")
+ val y = VariableLabel("y")
+ val x1 = VariableLabel("x'")
+ val y1 = VariableLabel("y'")
+ val z = VariableLabel("z")
+ val g = SchematicFunctionLabel("g", 0)
+ val h = SchematicPredicateLabel("h", 0)
+ val pxy = pair(x, y)
+ val pxy1 = pair(x1, y1)
+ val p0 = SCSubproof(
+ {
+ val p0 = SCSubproof(
+ {
+ val zf = in(z, pxy)
+ val p1_0 = hypothesis(zf)
+ val p1_1 = RightImplies(emptySeq +> (zf ==> zf), 0, zf, zf)
+ val p1_2 = RightIff(emptySeq +> (zf <=> zf), 1, 1, zf, zf) // |- (z in {x,y} <=> z in {x,y})
+ val p1_3 = RightSubstEq(emptySeq +< (pxy === pxy1) +> (zf <=> in(z, pxy1)), 2, List((pxy, pxy1)), LambdaTermFormula(Seq(g), zf <=> in(z, g())))
+ Proof(IndexedSeq(p1_0, p1_1, p1_2, p1_3), IndexedSeq(() |- pairAxiom))
+ },
+ Seq(-1),
+ display = true
+ ) // ({x,y}={x',y'}) |- ((z∈{x,y})↔(z∈{x',y'}))
+ val p1 = SCSubproof(
+ {
+ val p1_0 = Rewrite(() |- pairAxiom, -1) // |- ∀∀∀((z$1∈{x$3,y$2})↔((x$3=z$1)∨(y$2=z$1)))
+ val p1_1 = instantiateForall(Proof(IndexedSeq(p1_0), IndexedSeq(() |- pairAxiom)), x, y, z)
+ p1_1
+ },
+ Seq(-1),
+ display = true
+ ) // |- (z in {x,y}) <=> (z=x \/ z=y)
+ val p2 = SCSubproof(
+ {
+ val p2_0 = Rewrite(() |- pairAxiom, -1) // |- ∀∀∀((z$1∈{x$3,y$2})↔((x$3=z$1)∨(y$2=z$1)))
+ val p2_1 = instantiateForall(Proof(IndexedSeq(p2_0), IndexedSeq(() |- pairAxiom)), x1, y1, z)
+ p2_1
+ },
+ Seq(-1)
+ ) // |- (z in {x',y'}) <=> (z=x' \/ z=y')
+ val p3 = RightSubstEq(
+ emptySeq +< (pxy === pxy1) +> (in(z, pxy1) <=> ((z === x) \/ (z === y))),
+ 1,
+ List((pxy, pxy1)),
+ LambdaTermFormula(Seq(g), in(z, g()) <=> ((z === x) \/ (z === y)))
+ ) // ({x,y}={x',y'}) |- ((z∈{x',y'})↔((z=x)∨(z=y)))
+ val p4 = RightSubstIff(
+ emptySeq +< p3.bot.left.head +< p2.bot.right.head +> (((z === x) \/ (z === y)) <=> ((z === x1) \/ (z === y1))),
+ 3,
+ List(((z === x1) \/ (z === y1), in(z, pxy1))),
+ LambdaFormulaFormula(Seq(h), h() <=> ((z === x) \/ (z === y)))
+ ) // ((z∈{x',y'})↔((x'=z)∨(y'=z))), ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
+ val p5 = Cut(emptySeq ++< p3.bot ++> p4.bot, 2, 4, p2.bot.right.head)
+ Proof(IndexedSeq(p0, p1, p2, p3, p4, p5), IndexedSeq(() |- pairAxiom))
+ },
+ Seq(-1)
+ ) // ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
+
+ val p1 = SCSubproof(
+ Proof(
+ byCase(x === x1)(
+ SCSubproof(
+ {
+ val pcm1 = p0
+ val pc0 = SCSubproof(
+ Proof(
+ byCase(y === x)(
+ SCSubproof(
+ {
+ val pam1 = pcm1
+ val pa0 = SCSubproof(
+ {
+ val f1 = z === x
+ val pa0_m1 = pcm1 // ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
+ val pa0_0 = SCSubproof(
+ {
+ val pa0_0_0 = hypothesis(f1)
+ val pa0_1_1 = RightOr(emptySeq +< f1 +> (f1 \/ f1), 0, f1, f1)
+ val pa0_1_2 = RightImplies(emptySeq +> (f1 ==> (f1 \/ f1)), 1, f1, f1 \/ f1)
+ val pa0_1_3 = LeftOr(emptySeq +< (f1 \/ f1) +> f1, Seq(0, 0), Seq(f1, f1))
+ val pa0_1_4 = RightImplies(emptySeq +> ((f1 \/ f1) ==> f1), 3, f1 \/ f1, f1)
+ val pa0_1_5 = RightIff(emptySeq +> ((f1 \/ f1) <=> f1), 2, 4, (f1 \/ f1), f1)
+ val r = Proof(pa0_0_0, pa0_1_1, pa0_1_2, pa0_1_3, pa0_1_4, pa0_1_5)
+ r
+ },
+ display = false
+ ) // |- (((z=x)∨(z=x))↔(z=x))
+ val pa0_1 = RightSubstEq(
+ emptySeq +< (pxy === pxy1) +< (x === y) +> ((f1 \/ f1) <=> (z === x1) \/ (z === y1)),
+ -1,
+ List((x, y)),
+ LambdaTermFormula(Seq(g), (f1 \/ (z === g())) <=> ((z === x1) \/ (z === y1)))
+ ) // ({x,y}={x',y'}) y=x|- (z=x)\/(z=x) <=> (z=x' \/ z=y')
+ val pa0_2 = RightSubstIff(
+ emptySeq +< (pxy === pxy1) +< (x === y) +< (f1 <=> (f1 \/ f1)) +> (f1 <=> ((z === x1) \/ (z === y1))),
+ 1,
+ List((f1, f1 \/ f1)),
+ LambdaFormulaFormula(Seq(h), h() <=> ((z === x1) \/ (z === y1)))
+ )
+ val pa0_3 =
+ Cut(emptySeq +< (pxy === pxy1) +< (x === y) +> (f1 <=> ((z === x1) \/ (z === y1))), 0, 2, f1 <=> (f1 \/ f1)) // (x=y), ({x,y}={x',y'}) |- ((z=x)↔((z=x')∨(z=y')))
+ val pa0_4 = RightForall(emptySeq +< (pxy === pxy1) +< (x === y) +> forall(z, f1 <=> ((z === x1) \/ (z === y1))), 3, f1 <=> ((z === x1) \/ (z === y1)), z)
+ val ra0_0 = instantiateForall(Proof(IndexedSeq(pa0_0, pa0_1, pa0_2, pa0_3, pa0_4), IndexedSeq(pa0_m1.bot)), y1) // (x=y), ({x,y}={x',y'}) |- ((y'=x)↔((y'=x')∨(y'=y')))
+ ra0_0
+ },
+ IndexedSeq(-1)
+ ) // ({x,y}={x',y'}) y=x|- ((y'=x)↔((y'=x')∨(y'=y')))
+ val pa1 = SCSubproof(
+ {
+ val pa1_0 = RightRefl(emptySeq +> (y1 === y1), y1 === y1)
+ val pa1_1 = RightOr(emptySeq +> ((y1 === y1) \/ (y1 === x1)), 0, y1 === y1, y1 === x1)
+ Proof(pa1_0, pa1_1)
+ },
+ display = false
+ ) // |- (y'=x' \/ y'=y')
+ val ra3 = byEquiv(pa0.bot.right.head, pa1.bot.right.head)(pa0, pa1) // ({x,y}={x',y'}) y=x|- ((y'=x)
+ val pal = RightSubstEq(emptySeq ++< pa0.bot +> (y1 === y), ra3.length - 1, List((x, y)), LambdaTermFormula(Seq(g), y1 === g()))
+ Proof(ra3.steps, IndexedSeq(pam1.bot)).appended(pal) // (x=y), ({x,y}={x',y'}) |- (y'=y)
+ },
+ IndexedSeq(-1)
+ ) // (x=y), ({x,y}={x',y'}) |- (y'=y)
+ ,
+ SCSubproof(
+ {
+ val pbm1 = pcm1 // ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
+ val pb0_0 = SCSubproof(
+ {
+ val pb0_0 = RightForall(emptySeq ++< pcm1.bot +> forall(z, pcm1.bot.right.head), -1, pcm1.bot.right.head, z)
+ instantiateForall(Proof(IndexedSeq(pb0_0), IndexedSeq(pcm1.bot)), y)
+ },
+ IndexedSeq(-1)
+ ) // ({x,y}={x',y'}) |- (((y=x)∨(y=y))↔((y=x')∨(y=y')))
+ val pb0_1 = SCSubproof(
+ {
+ val pa1_0 = RightRefl(emptySeq +> (y === y), y === y)
+ val pa1_1 = RightOr(emptySeq +> ((y === y) \/ (y === x)), 0, y === y, y === x)
+ Proof(pa1_0, pa1_1)
+ },
+ display = false
+ ) // |- (y=x)∨(y=y)
+ val rb0 = byEquiv(pb0_0.bot.right.head, pb0_1.bot.right.head)(pb0_0, pb0_1) // ({x,y}={x',y'}) |- (y=x')∨(y=y')
+ val pb1 =
+ RightSubstEq(emptySeq ++< rb0.conclusion +< (x === x1) +> ((y === x) \/ (y === y1)), rb0.length - 1, List((x, x1)), LambdaTermFormula(Seq(g), (y === g()) \/ (y === y1)))
+ val rb1 = destructRightOr(
+ rb0.appended(pb1), // ({x,y}={x',y'}) , x=x'|- (y=x)∨(y=y')
+ y === x,
+ y === y1
+ )
+ val rb2 = rb1.appended(LeftNot(rb1.conclusion +< !(y === x) -> (y === x), rb1.length - 1, y === x)) // (x=x'), ({x,y}={x',y'}), ¬(y=x) |- (y=y')
+ Proof(rb2.steps, IndexedSeq(pbm1.bot))
+
+ },
+ IndexedSeq(-1)
+ ) // ({x,y}={x',y'}), x=x', !y=x |- y=y'
+ ).steps,
+ IndexedSeq(pcm1.bot)
+ ),
+ IndexedSeq(-1)
+ ) // (x=x'), ({x,y}={x',y'}) |- (y'=y)
+ val pc1 = RightRefl(emptySeq +> (x === x), x === x)
+ val pc2 = RightAnd(emptySeq ++< pc0.bot +> ((y1 === y) /\ (x === x)), Seq(0, 1), Seq(y1 === y, x === x)) // ({x,y}={x',y'}), x=x' |- (x=x /\ y=y')
+ val pc3 =
+ RightSubstEq(emptySeq ++< pc2.bot +> ((y1 === y) /\ (x1 === x)), 2, List((x, x1)), LambdaTermFormula(Seq(g), (y1 === y) /\ (g() === x))) // ({x,y}={x',y'}), x=x' |- (x=x' /\ y=y')
+ val pc4 = RightOr(
+ emptySeq ++< pc3.bot +> (pc3.bot.right.head \/ ((x === y1) /\ (y === x1))),
+ 3,
+ pc3.bot.right.head,
+ (x === y1) /\ (y === x1)
+ ) // ({x,y}={x',y'}), x=x' |- (x=x' /\ y=y')\/(x=y' /\ y=x')
+ val r = Proof(IndexedSeq(pc0, pc1, pc2, pc3, pc4), IndexedSeq(pcm1.bot))
+ r
+ },
+ IndexedSeq(-1)
+ ) // ({x,y}={x',y'}), x=x' |- (x=x' /\ y=y')\/(x=y' /\ y=x')
+ ,
+ SCSubproof(
+ {
+ val pdm1 = p0
+ val pd0 = SCSubproof(
+ {
+ val pd0_m1 = pdm1
+ val pd0_0 = SCSubproof {
+ val ex1x1 = x1 === x1
+ val pd0_0_0 = RightRefl(emptySeq +> ex1x1, ex1x1) // |- x'=x'
+ val pd0_0_1 = RightOr(emptySeq +> (ex1x1 \/ (x1 === y1)), 0, ex1x1, x1 === y1) // |- (x'=x' \/ x'=y')
+ Proof(IndexedSeq(pd0_0_0, pd0_0_1))
+ } // |- (x'=x' \/ x'=y')
+ val pd0_1 = SCSubproof(
+ {
+ val pd0_1_m1 = pd0_m1 // ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
+ val pd0_1_0 = RightForall(emptySeq ++< pd0_1_m1.bot +> forall(z, pd0_1_m1.bot.right.head), -1, pd0_1_m1.bot.right.head, z)
+ val rd0_1_1 = instantiateForall(Proof(IndexedSeq(pd0_1_0), IndexedSeq(pd0_m1.bot)), x1) // ({x,y}={x',y'}) |- (x'=x \/ x'=y) <=> (x'=x' \/ x'=y')
+ rd0_1_1
+ },
+ IndexedSeq(-1)
+ ) // ({x,y}={x',y'}) |- (x'=x \/ x'=y) <=> (x'=x' \/ x'=y')
+ val pd0_2 = RightSubstIff(
+ pd0_1.bot.right |- ((x1 === x) \/ (x1 === y)),
+ 0,
+ List(((x1 === x) \/ (x1 === y), (x1 === x1) \/ (x1 === y1))),
+ LambdaFormulaFormula(Seq(h), h())
+ ) // (x'=x \/ x'=y) <=> (x'=x' \/ x'=y') |- (x'=x \/ x'=y)
+ val pd0_3 = Cut(pd0_1.bot.left |- pd0_2.bot.right, 1, 2, pd0_1.bot.right.head) // ({x,y}={x',y'}) |- (x=x' \/ y=x')
+ destructRightOr(Proof(IndexedSeq(pd0_0, pd0_1, pd0_2, pd0_3), IndexedSeq(pd0_m1.bot)), x === x1, y === x1) // ({x,y}={x',y'}) |- x=x', y=x'
+ },
+ IndexedSeq(-1)
+ ) // ({x,y}={x',y'}) |- x=x', y=x' --
+ val pd1 = SCSubproof(
+ {
+ val pd1_m1 = pdm1
+ val pd1_0 = SCSubproof {
+ val exx = x === x
+ val pd1_0_0 = RightRefl(emptySeq +> exx, exx) // |- x=x
+ val pd1_0_1 = RightOr(emptySeq +> (exx \/ (x === y)), 0, exx, x === y) // |- (x=x \/ x=y)
+ Proof(IndexedSeq(pd1_0_0, pd1_0_1))
+ } // |- (x=x \/ x=y)
+ val pd1_1 = SCSubproof(
+ {
+ val pd1_1_m1 = pd1_m1 // ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
+ val pd1_1_0 = RightForall(emptySeq ++< pd1_1_m1.bot +> forall(z, pd1_1_m1.bot.right.head), -1, pd1_1_m1.bot.right.head, z)
+ val rd1_1_1 = instantiateForall(Proof(IndexedSeq(pd1_1_0), IndexedSeq(pd1_m1.bot)), x) // ({x,y}={x',y'}) |- (x=x \/ x=y) <=> (x=x' \/ x=y')
+ rd1_1_1
+ },
+ IndexedSeq(-1)
+ ) // // ({x,y}={x',y'}) |- (x=x \/ x=y) <=> (x=x' \/ x=y')
+ val rd1_2 = byEquiv(pd1_1.bot.right.head, pd1_0.bot.right.head)(pd1_1, pd1_0)
+ val pd1_3 = SCSubproof(Proof(rd1_2.steps, IndexedSeq(pd1_m1.bot)), IndexedSeq(-1)) // // ({x,y}={x',y'}) |- x=x' \/ x=y'
+ destructRightOr(Proof(IndexedSeq(pd1_0, pd1_1, pd1_3), IndexedSeq(pd1_m1.bot)), x === x1, x === y1) // ({x,y}={x',y'}) |- x=x', x=y'
+ },
+ IndexedSeq(-1)
+ ) // ({x,y}={x',y'}) |- x=x', x=y' --
+ val pd2 = RightAnd(emptySeq ++< pd1.bot +> (x === x1) +> ((x === y1) /\ (y === x1)), Seq(0, 1), Seq(x === y1, y === x1)) // ({x,y}={x',y'}) |- x=x', (x=y' /\ y=x') ---
+ val pd3 = LeftNot(emptySeq ++< pd2.bot +< !(x === x1) +> ((x === y1) /\ (y === x1)), 2, x === x1) // ({x,y}={x',y'}), !x===x1 |- (x=y' /\ y=x')
+ val pd4 = RightOr(
+ emptySeq ++< pd3.bot +> (pd3.bot.right.head \/ ((x === x1) /\ (y === y1))),
+ 3,
+ pd3.bot.right.head,
+ (x === x1) /\ (y === y1)
+ ) // ({x,y}={x',y'}), !x===x1 |- (x=x' /\ y=y')\/(x=y' /\ y=x')
+ Proof(IndexedSeq(pd0, pd1, pd2, pd3, pd4), IndexedSeq(pdm1.bot))
+ },
+ IndexedSeq(-1)
+ ) // ({x,y}={x',y'}), !x=x' |- (x=x' /\ y=y')\/(x=y' /\ y=x')
+ ).steps,
+ IndexedSeq(p0.bot)
+ ),
+ IndexedSeq(0)
+ ) // ({x,y}={x',y'}) |- (x=x' /\ y=y')\/(x=y' /\ y=x')
+
+ val p2 = RightImplies(emptySeq +> (p1.bot.left.head ==> p1.bot.right.head), 1, p1.bot.left.head, p1.bot.right.head) // |- ({x,y}={x',y'}) ==> (x=x' /\ y=y')\/(x=y' /\ y=x')
+ generalizeToForall(Proof(IndexedSeq(p0, p1, p2), IndexedSeq(() |- pairAxiom)), x, y, x1, y1)
+ } using ax"pairAxiom"
+ thm"unorderedPair_deconstruction".show
+
+ THEOREM("noUniversalSet") of "∀x. x ∈ ?z ⊢" PROOF {
+ val x = SchematicFunctionLabel("x", 0)
+ val z = SchematicFunctionLabel("z", 0)
+ val x1 = VariableLabel("x")
+ val y1 = VariableLabel("y")
+ val z1 = VariableLabel("z")
+ val h = SchematicPredicateLabel("h", 0)
+ val sPhi = SchematicPredicateLabel("P", 2)
+ // forall(z, exists(y, forall(x, in(x,y) <=> (in(x,y) /\ sPhi(x,z)))))
+ val i1 = () |- comprehensionSchema
+ val i2 = thm"russelParadox" // forall(x1, in(x1,y) <=> !in(x1, x1)) |- ()
+ val p0 = InstPredSchema(() |- forall(z1, exists(y1, forall(x1, in(x1, y1) <=> (in(x1, z1) /\ !in(x1, x1))))), -1, Map(sPhi -> LambdaTermFormula(Seq(x, z), !in(x(), x()))))
+ val s0 = SCSubproof(instantiateForall(Proof(IndexedSeq(p0), IndexedSeq(i1)), z), Seq(-1)) // exists(y1, forall(x1, in(x1,y1) <=> (in(x1,z1) /\ !in(x1, x1))))
+ val s1 = hypothesis(in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1))) // in(x,y) <=> (in(x,z) /\ in(x, x)) |- in(x,y) <=> (in(x,z) /\ in(x, x))
+ val s2 = RightSubstIff(
+ (in(x1, z) <=> And(), in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1))) |- in(x1, y1) <=> (And() /\ !in(x1, x1)),
+ 1,
+ List((in(x1, z), And())),
+ LambdaFormulaFormula(Seq(h), in(x1, y1) <=> (h() /\ !in(x1, x1)))
+ ) // in(x1,y1) <=> (in(x1,z1) /\ in(x1, x1)) |- in(x,y) <=> (And() /\ in(x1, x1))
+ val s3 = Rewrite((in(x1, z), in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1))) |- in(x1, y1) <=> !in(x1, x1), 2)
+ val s4 = LeftForall((forall(x1, in(x1, z)), in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1))) |- in(x1, y1) <=> !in(x1, x1), 3, in(x1, z), x1, x1)
+ val s5 = LeftForall((forall(x1, in(x1, z)), forall(x1, in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1)))) |- in(x1, y1) <=> !in(x1, x1), 4, in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1)), x1, x1)
+ val s6 = RightForall((forall(x1, in(x1, z)), forall(x1, in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1)))) |- forall(x1, in(x1, y1) <=> !in(x1, x1)), 5, in(x1, y1) <=> !in(x1, x1), x1)
+ val s7 = InstFunSchema(forall(x1, in(x1, y1) <=> !in(x1, x1)) |- (), -2, Map(SchematicFunctionLabel("y", 0) -> LambdaTermTerm(Nil, y1)))
+ val s8 = Cut((forall(x1, in(x1, z)), forall(x1, in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1)))) |- (), 6, 7, forall(x1, in(x1, y1) <=> !in(x1, x1)))
+ val s9 = LeftExists((forall(x1, in(x1, z)), exists(y1, forall(x1, in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1))))) |- (), 8, forall(x1, in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1))), y1)
+ val s10 = Cut(forall(x1, in(x1, z)) |- (), 0, 9, exists(y1, forall(x1, in(x1, y1) <=> (in(x1, z) /\ !in(x1, x1)))))
+ Proof(steps(s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10), imports(i1, i2))
+ } using (ax"comprehensionSchema", thm"russelParadox")
+ show
+
+ private val sx = SchematicFunctionLabel("x", 0)
+ private val sy = SchematicFunctionLabel("y", 0)
+ val oPair: ConstantFunctionLabel = DEFINE("", sx, sy) as pair(pair(sx, sy), pair(sx, sx))
+ show
+
+}
diff --git a/src/main/scala/proven/tactics/ProofTactics.scala b/src/main/scala/proven/tactics/ProofTactics.scala
index d367cf93899006d21b4565beb931ab62e74c84c2..dde13d44e93ce53c4f5b5c94f1e047a7a432b3c0 100644
--- a/src/main/scala/proven/tactics/ProofTactics.scala
+++ b/src/main/scala/proven/tactics/ProofTactics.scala
@@ -3,7 +3,7 @@ package proven.tactics
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SequentCalculus.*
-import utilities.Helpers.{*, given}
+import utilities.Helpers.{_, given}
import utilities.Printer.*
import scala.collection.immutable.Set
@@ -72,17 +72,17 @@ object ProofTactics {
}
@deprecated
- def simpleFunctionDefinition(expression:LambdaTermTerm, out:VariableLabel): SCProof = {
+ def simpleFunctionDefinition(expression: LambdaTermTerm, out: VariableLabel): SCProof = {
val x = out
val LambdaTermTerm(vars, body) = expression
- val xeb = x===body
- val y = VariableLabel(freshId(body.freeVariables.map(_.id)++vars.map(_.id), "y"))
+ val xeb = x === body
+ val y = VariableLabel(freshId(body.freeVariables.map(_.id) ++ vars.map(_.id), "y"))
val s0 = RightRefl(() |- body === body, body === body)
val s1 = Rewrite(() |- (xeb) <=> (xeb), 0)
val s2 = RightForall(() |- forall(x, (xeb) <=> (xeb)), 1, (xeb) <=> (xeb), x)
val s3 = RightExists(() |- exists(y, forall(x, (x === y) <=> (xeb))), 2, forall(x, (x === y) <=> (xeb)), y, body)
val s4 = Rewrite(() |- existsOne(x, xeb), 3)
- val v = Vector(s0, s1, s2, s3, s4)/*
+ val v = Vector(s0, s1, s2, s3, s4) /*
val v2 = args.foldLeft((v, s4.bot.right.head, 4))((prev, x) => {
val fo = forall(x, prev._2)
(prev._1 appended RightForall(emptySeq +> fo, prev._3, prev._2, x), fo, prev._3 + 1)
diff --git a/src/main/scala/utilities/Helpers.scala b/src/main/scala/utilities/Helpers.scala
index 61e801dec3ca7fea43a752261436614b418bb98c..a69647319951f6352dc7753a67506d3820927ff2 100644
--- a/src/main/scala/utilities/Helpers.scala
+++ b/src/main/scala/utilities/Helpers.scala
@@ -1,3 +1,10 @@
package utilities
+/**
+ * A helper file that provides various syntactic sugars for LISA's FOL and proofs.
+ * Usage:
+ * <pre>
+ * import utilities.Helpers.*
+ * </pre>
+ */
object Helpers extends TheoriesHelpers {}
diff --git a/src/main/scala/utilities/KernelHelpers.scala b/src/main/scala/utilities/KernelHelpers.scala
index 754d3f1837e57a0ede8cb5109cfabb63c48f15c0..5dd3793c8aad2a2ddc5529540fa3b699c67ecbfd 100644
--- a/src/main/scala/utilities/KernelHelpers.scala
+++ b/src/main/scala/utilities/KernelHelpers.scala
@@ -1,15 +1,22 @@
package utilities
-import lisa.kernel.proof.{RunningTheory, RunningTheoryJudgement, SCProof, SequentCalculus}
+import lisa.kernel.proof.RunningTheory
+import lisa.kernel.proof.RunningTheoryJudgement
import lisa.kernel.proof.RunningTheoryJudgement.InvalidJustification
+import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SequentCalculus
import lisa.kernel.proof.SequentCalculus.Rewrite
import lisa.kernel.proof.SequentCalculus.isSameSequent
/**
- * A helper file that provides various syntactic sugars for LISA.
+ * A helper file that provides various syntactic sugars for LISA's FOL and proofs. Best imported through utilities.Helpers
* Usage:
* <pre>
- * import lisa.KernelHelpers.*
+ * import utilities.Helpers.*
+ * </pre>
+ * or
+ * <pre>
+ * extends utilities.KernelHelpers.*
* </pre>
*/
trait KernelHelpers {
@@ -81,18 +88,12 @@ trait KernelHelpers {
given Conversion[VariableLabel, VariableTerm] = VariableTerm.apply
given Conversion[VariableTerm, VariableLabel] = _.label
-
given Conversion[PredicateFormula, PredicateLabel] = _.label
-
given Conversion[FunctionTerm, FunctionLabel] = _.label
-
given Conversion[SchematicFunctionLabel, Term] = _.apply()
-
- // given Conversion[Tuple, List[Union[_.type]]] = _.toList
-
given Conversion[(Boolean, List[Int], String), Option[(List[Int], String)]] = tr => if (tr._1) None else Some(tr._2, tr._3)
-
given Conversion[Formula, Sequent] = () |- _
+
/* Sequents */
val emptySeq: Sequent = Sequent(Set.empty, Set.empty)
diff --git a/src/main/scala/utilities/Library.scala b/src/main/scala/utilities/Library.scala
index 571807aae49c0bd4ecb992b71264d348cc5f9c44..18a5fdad92df9753423c714187269c094af5420b 100644
--- a/src/main/scala/utilities/Library.scala
+++ b/src/main/scala/utilities/Library.scala
@@ -1,146 +1,231 @@
package utilities
-import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.RunningTheory
-import lisa.kernel.proof.RunningTheoryJudgement
-import lisa.kernel.proof.SCProof
-import lisa.kernel.proof.SequentCalculus.*
-import Helpers.{*, given}
-import lisa.settheory.AxiomaticSetTheory.pair
-import proven.tactics.ProofTactics.simpleFunctionDefinition
+/**
+ * A class abstracting a [[lisa.kernel.proof.RunningTheory]] providing utility functions and a convenient syntax
+ * to write and use Theorems and Definitions.
+ * @param theory The inner RunningTheory
+ */
abstract class Library(val theory: RunningTheory) {
- val realOutput: String => Unit
-
- type Proof = SCProof
- val Proof = SCProof
- type Justification = theory.Justification
- type Theorem = theory.Theorem
- val Theorem = theory.Theorem
- type Definition = theory.Definition
- type Axiom = theory.Axiom
- val Axiom = theory.Axiom
- type PredicateDefinition = theory.PredicateDefinition
- val PredicateDefinition = theory.PredicateDefinition
- type FunctionDefinition = theory.FunctionDefinition
- val FunctionDefinition = theory.FunctionDefinition
- type Judgement[J <: Justification] = RunningTheoryJudgement[J]
-
-
+ given RunningTheory = theory
+ export lisa.kernel.fol.FOL.*
+ export lisa.kernel.proof.SequentCalculus.*
+ export lisa.kernel.proof.SCProof as Proof
+ export theory.{Justification, Theorem, Definition, Axiom, PredicateDefinition, FunctionDefinition}
+ export Helpers.{*, given}
+ import lisa.kernel.proof.RunningTheoryJudgement as Judgement
+
+ /**
+ * a type representing different types that have a natural representation as Sequent
+ */
type Sequentable = Justification | Formula | Sequent
- private var last :Option[Justification] = None
-
- private var outString :List[String] = List()
- private val lineBreak = "\n"
- given output: (String => Unit) = s => outString = lineBreak :: s :: outString
-
+ private var last: Option[Justification] = None
+ /**
+ * A function intended for use to construct a proof:
+ * <pre> Proof(steps(...), imports(...))</pre>
+ * Must contains [[SCProofStep]]'s
+ */
+ inline def steps(sts: SCProofStep*): IndexedSeq[SCProofStep] = sts.toIndexedSeq
- inline def steps(sts:SCProofStep*):IndexedSeq[SCProofStep] = sts.toIndexedSeq
- inline def imports(sqs:Sequentable*):IndexedSeq[Sequent] = sqs.map(sequantableToSequent).toIndexedSeq
- // extension (s:String) def apply():Unit = ()
-
+ /**
+ * A function intended for use to construct a proof:
+ * <pre> Proof(steps(...), imports(...))</pre>
+ * Must contains [[Justification]]'s, [[Formula]]'s or [[Sequent]], all of which are converted adequatly automatically.
+ */
+ inline def imports(sqs: Sequentable*): IndexedSeq[Sequent] = sqs.map(sequantableToSequent).toIndexedSeq
// THEOREM Syntax
- def makeTheorem(name: String, statement: String, proof: SCProof, justifications: Seq[theory.Justification]): RunningTheoryJudgement[theory.Theorem] =
+
+ /**
+ * An alias to create a Theorem
+ */
+ def makeTheorem(name: String, statement: String, proof: Proof, justifications: Seq[theory.Justification]): Judgement[theory.Theorem] =
theory.theorem(name, statement, proof, justifications)
+ /**
+ * Syntax: <pre> THEOREM("name") of "the sequent concluding the proof" PROOF { the proof } using (assumptions) </pre>
+ */
case class TheoremNameWithStatement(name: String, statement: String) {
- def PROOF(proof: SCProof): TheoremNameWithProof = TheoremNameWithProof(name, statement, proof)
+
+ /**
+ * Syntax: <pre> THEOREM("name") of "the sequent concluding the proof" PROOF { the proof } using (assumptions) </pre>
+ */
+ def PROOF(proof: Proof)(using String => Unit): TheoremNameWithProof = TheoremNameWithProof(name, statement, proof)
+
+ /**
+ * Syntax: <pre> THEOREM("name") of "the sequent concluding the proof" PROOF { the proof } using (assumptions) </pre>
+ */
+ def PROOF(steps: IndexedSeq[SCProofStep])(using String => Unit): TheoremNameWithProof = TheoremNameWithProof(name, statement, Proof(steps))
}
+ /**
+ * Syntax: <pre> THEOREM("name") of "the sequent concluding the proof" PROOF { the proof } using (assumptions) </pre>
+ */
case class TheoremName(name: String) {
+ /**
+ * Syntax: <pre> THEOREM("name") of "the sequent concluding the proof" PROOF { the proof } using (assumptions) </pre>
+ */
infix def of(statement: String): TheoremNameWithStatement = TheoremNameWithStatement(name, statement)
}
+ /**
+ * Syntax: <pre> THEOREM("name") of "the sequent concluding the proof" PROOF { the proof } using (assumptions) </pre>
+ */
def THEOREM(name: String): TheoremName = TheoremName(name)
- case class TheoremNameWithProof(name: String, statement: String, proof: SCProof) {
+ /**
+ * Syntax: <pre> THEOREM("name") of "the sequent concluding the proof" PROOF { the proof } using (assumptions) </pre>
+ */
+ case class TheoremNameWithProof(name: String, statement: String, proof: Proof)(using String => Unit) {
infix def using(justifications: theory.Justification*): theory.Theorem = theory.theorem(name, statement, proof, justifications) match
- case RunningTheoryJudgement.ValidJustification(just) =>
+ case Judgement.ValidJustification(just) =>
last = Some(just)
just
- case wrongJudgement: RunningTheoryJudgement.InvalidJustification[_] => wrongJudgement.showAndGet(output)
+ case wrongJudgement: Judgement.InvalidJustification[_] => wrongJudgement.showAndGet
+ /**
+ * Syntax: <pre> THEOREM("name") of "the sequent concluding the proof" PROOF { the proof } using (assumptions) </pre>
+ */
infix def using(u: Unit): theory.Theorem = using()
}
+ // DEFINITION Syntax
- //DEFINITION Syntax
- def simpleDefinition(symbol:String, expression: LambdaTermTerm): RunningTheoryJudgement[theory.FunctionDefinition] =
+ /**
+ * Allows to create a definition by shortcut of a function symbol:
+ */
+ def simpleDefinition(symbol: String, expression: LambdaTermTerm): Judgement[theory.FunctionDefinition] =
val LambdaTermTerm(vars, body) = expression
- val out:VariableLabel = VariableLabel(freshId((vars.map(_.id)++body.schematicFunctions.map(_.id)).toSet, "y"))
- val proof:Proof = simpleFunctionDefinition(expression, out)
+ val out: VariableLabel = VariableLabel(freshId((vars.map(_.id) ++ body.schematicFunctions.map(_.id)).toSet, "y"))
+ val proof: Proof = simpleFunctionDefinition(expression, out)
theory.functionDefinition(symbol, LambdaTermFormula(vars, out === body), out, proof, Nil)
- def complexDefinition(symbol:String, vars:Seq[SchematicFunctionLabel], v:SchematicFunctionLabel, f:Formula, proof:Proof, just:Seq[Justification]): RunningTheoryJudgement[theory.FunctionDefinition] =
- val out:VariableLabel = VariableLabel(freshId((vars.map(_.id)++f.schematicFunctions.map(_.id)).toSet, "y"))
+ /**
+ * Allows to create a definition by existential uniqueness of a function symbol:
+ */
+ def complexDefinition(symbol: String, vars: Seq[SchematicFunctionLabel], v: SchematicFunctionLabel, f: Formula, proof: Proof, just: Seq[Justification]): Judgement[theory.FunctionDefinition] =
+ val out: VariableLabel = VariableLabel(freshId((vars.map(_.id) ++ f.schematicFunctions.map(_.id)).toSet, "y"))
theory.functionDefinition(symbol, LambdaTermFormula(vars, instantiateFunctionSchemas(f, Map(v -> LambdaTermTerm(Nil, out)))), out, proof, just)
- def simpleDefinition(symbol:String, expression: LambdaTermFormula): RunningTheoryJudgement[theory.PredicateDefinition] =
+ /**
+ * Allows to create a definition by shortcut of a function symbol:
+ */
+ def simpleDefinition(symbol: String, expression: LambdaTermFormula): Judgement[theory.PredicateDefinition] =
theory.predicateDefinition(symbol, expression)
- case class FunSymbolDefine(symbol:String, vars:Seq[SchematicFunctionLabel]){
- infix def as(t:Term): ConstantFunctionLabel =
+ /**
+ * Syntax: <pre> DEFINE("symbol", arguments) as "definition" </pre>
+ * or
+ * Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre>
+ */
+ case class FunSymbolDefine(symbol: String, vars: Seq[SchematicFunctionLabel]) {
+
+ /**
+ * Syntax: <pre> DEFINE("symbol", arguments) as "definition" </pre>
+ */
+ infix def as(t: Term)(using String => Unit): ConstantFunctionLabel =
val definition = simpleDefinition(symbol, LambdaTermTerm(vars, t)) match
- case RunningTheoryJudgement.ValidJustification(just) =>
+ case Judgement.ValidJustification(just) =>
last = Some(just)
just
- case wrongJudgement: RunningTheoryJudgement.InvalidJustification[_] => wrongJudgement.showAndGet(realOutput)
+ case wrongJudgement: Judgement.InvalidJustification[_] => wrongJudgement.showAndGet
definition.label
- infix def as(f:Formula): ConstantPredicateLabel =
+
+ /**
+ * Syntax: <pre> DEFINE("symbol", arguments) as "definition" </pre>
+ */
+ infix def as(f: Formula)(using String => Unit): ConstantPredicateLabel =
val definition = simpleDefinition(symbol, LambdaTermFormula(vars, f)) match
- case RunningTheoryJudgement.ValidJustification(just) =>
+ case Judgement.ValidJustification(just) =>
last = Some(just)
just
- case wrongJudgement: RunningTheoryJudgement.InvalidJustification[_] => wrongJudgement.showAndGet(realOutput)
+ case wrongJudgement: Judgement.InvalidJustification[_] => wrongJudgement.showAndGet
definition.label
- infix def asThe(out:SchematicFunctionLabel):DefinitionNameAndOut = DefinitionNameAndOut(symbol, vars, out)
+ /**
+ * Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre>
+ */
+ infix def asThe(out: SchematicFunctionLabel): DefinitionNameAndOut = DefinitionNameAndOut(symbol, vars, out)
}
- case class DefinitionNameAndOut(symbol:String, vars:Seq[SchematicFunctionLabel], out:SchematicFunctionLabel){
- infix def suchThat (f:Formula):DefinitionWaitingProof = DefinitionWaitingProof(symbol, vars, out, f)
+ /**
+ * Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre>
+ */
+ case class DefinitionNameAndOut(symbol: String, vars: Seq[SchematicFunctionLabel], out: SchematicFunctionLabel) {
+
+ /**
+ * Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre>
+ */
+ infix def suchThat(f: Formula): DefinitionWaitingProof = DefinitionWaitingProof(symbol, vars, out, f)
}
- case class DefinitionWaitingProof(symbol:String, vars:Seq[SchematicFunctionLabel], out:SchematicFunctionLabel, f:Formula ){
- infix def PROOF(proof:SCProof):DefinitionWithProof = DefinitionWithProof(symbol, vars, out, f, proof)
+ /**
+ * Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre>
+ */
+ case class DefinitionWaitingProof(symbol: String, vars: Seq[SchematicFunctionLabel], out: SchematicFunctionLabel, f: Formula) {
+
+ /**
+ * Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre>
+ */
+ infix def PROOF(proof: Proof): DefinitionWithProof = DefinitionWithProof(symbol, vars, out, f, proof)
}
- case class DefinitionWithProof(symbol:String, vars:Seq[SchematicFunctionLabel], out:SchematicFunctionLabel, f:Formula, proof:Proof){
- infix def using(justifications: theory.Justification*): ConstantFunctionLabel =
+ /**
+ * Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre>
+ */
+ case class DefinitionWithProof(symbol: String, vars: Seq[SchematicFunctionLabel], out: SchematicFunctionLabel, f: Formula, proof: Proof) {
+
+ /**
+ * Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre>
+ */
+ infix def using(justifications: theory.Justification*)(using String => Unit): ConstantFunctionLabel =
val definition = complexDefinition(symbol, vars, out, f, proof, justifications) match
- case RunningTheoryJudgement.ValidJustification(just) =>
+ case Judgement.ValidJustification(just) =>
last = Some(just)
just
- case wrongJudgement: RunningTheoryJudgement.InvalidJustification[_] => wrongJudgement.showAndGet(realOutput)
+ case wrongJudgement: Judgement.InvalidJustification[_] => wrongJudgement.showAndGet
definition.label
- infix def using(u: Unit): ConstantFunctionLabel = using()
+ /**
+ * Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre>
+ */
+ infix def using(u: Unit)(using String => Unit): ConstantFunctionLabel = using()
}
- //DEFINE("+", sx, sy) asThe v suchThat ... PROOF {...} using ()
+ /**
+ * Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre>
+ */
+ def DEFINE(symbol: String, vars: SchematicFunctionLabel*): FunSymbolDefine = FunSymbolDefine(symbol, vars)
- def DEFINE(symbol:String, vars:SchematicFunctionLabel*): FunSymbolDefine = FunSymbolDefine(symbol, vars)
-
- def simpleFunctionDefinition(expression:LambdaTermTerm, out:VariableLabel): SCProof = {
+ /**
+ * For a definition of the type f(x) := term, construct the required proof ∃!y. y = term.
+ */
+ private def simpleFunctionDefinition(expression: LambdaTermTerm, out: VariableLabel): Proof = {
val x = out
val LambdaTermTerm(vars, body) = expression
- val xeb = x===body
- val y = VariableLabel(freshId(body.freeVariables.map(_.id)++vars.map(_.id)+out.id, "y"))
+ val xeb = x === body
+ val y = VariableLabel(freshId(body.freeVariables.map(_.id) ++ vars.map(_.id) + out.id, "y"))
val s0 = RightRefl(() |- body === body, body === body)
val s1 = Rewrite(() |- (xeb) <=> (xeb), 0)
val s2 = RightForall(() |- forall(x, (xeb) <=> (xeb)), 1, (xeb) <=> (xeb), x)
val s3 = RightExists(() |- exists(y, forall(x, (x === y) <=> (xeb))), 2, forall(x, (x === y) <=> (xeb)), y, body)
val s4 = Rewrite(() |- existsOne(x, xeb), 3)
val v = Vector(s0, s1, s2, s3, s4)
- SCProof(v)
+ Proof(v)
}
+ // Implicit conversions
+
given Conversion[TheoremNameWithProof, theory.Theorem] = _.using()
+ /**
+ * Allows to fetch a Justification (Axiom, Theorem or Definition) by it's name or symbol:
+ * <pre>thm"fundamentalTheoremOfAlgebra", ax"comprehensionAxiom", defi"+"
+ */
implicit class StringToJust(val sc: StringContext) {
def thm(args: Any*): theory.Theorem = getTheorem(sc.parts.mkString(""))
@@ -150,46 +235,59 @@ abstract class Library(val theory: RunningTheory) {
def defi(args: Any*): theory.Definition = getDefinition(sc.parts.mkString(""))
}
+ /**
+ * Fetch a Theorem by its name.
+ */
def getTheorem(name: String): theory.Theorem =
theory.getTheorem(name) match
case Some(value) => value
case None => throw java.util.NoSuchElementException(s"No theorem with name \"$name\" was found.")
+ /**
+ * Fetch an Axiom by its name.
+ */
def getAxiom(name: String): theory.Axiom =
theory.getAxiom(name) match
case Some(value) => value
case None => throw java.util.NoSuchElementException(s"No axiom with name \"$name\" was found.")
+ /**
+ * Fetch a Definition by its symbol.
+ */
def getDefinition(name: String): theory.Definition =
theory.getDefinition(name) match
case Some(value) => value
case None => throw java.util.NoSuchElementException(s"No definition for symbol \"$name\" was found.")
- def show: Justification = last match
+ /**
+ * Prints a short representation of the last theorem or definition introduced
+ */
+ def show(using String => Unit): Justification = last match
case Some(value) => value.show
case None => throw new NoSuchElementException("There is nothing to show: No theorem or definition has been proved yet.")
- //given Conversion[String, theory.Justification] = name => theory.getJustification(name).get
+ // given Conversion[String, theory.Justification] = name => theory.getJustification(name).get
- private def sequantableToSequent(s:Sequentable): Sequent= s match
- case j:Justification => theory.sequentFromJustification(j)
- case f:Formula => () |- f
- case s:Sequent => s
+ /**
+ * Converts different class that have a natural interpretation as a Sequent
+ */
+ private def sequantableToSequent(s: Sequentable): Sequent = s match
+ case j: Justification => theory.sequentFromJustification(j)
+ case f: Formula => () |- f
+ case s: Sequent => s
given Conversion[Sequentable, Sequent] = sequantableToSequent
- given Conversion[theory.Axiom, Formula] = theory.sequentFromJustification(_).right.head
- given Conversion[Formula, Axiom] = (f:Formula) => theory.getAxiom(f).get
- given convJustSequent[C <: Iterable[Sequentable], D](using bf: scala.collection.BuildFrom[C, Sequent, D]) : Conversion[C, D] = cc => {
+ given Conversion[Axiom, Formula] = theory.sequentFromJustification(_).right.head
+ given Conversion[Formula, Axiom] = (f: Formula) => theory.getAxiom(f).get
+ given convJustSequent[C <: Iterable[Sequentable], D](using bf: scala.collection.BuildFrom[C, Sequent, D]): Conversion[C, D] = cc => {
val builder = bf.newBuilder(cc)
cc.foreach(builder += sequantableToSequent(_))
builder.result
}
- given convStrInt[C <: Iterable[String], D](using bf: scala.collection.BuildFrom[C, Int, D]) : Conversion[C, D] = cc => {
+ given convStrInt[C <: Iterable[String], D](using bf: scala.collection.BuildFrom[C, Int, D]): Conversion[C, D] = cc => {
val builder = bf.newBuilder(cc)
cc.foreach(builder += _.size)
builder.result
}
- def main(args: Array[String]): Unit = { realOutput(outString.reverse.mkString("")) }
-
}
diff --git a/src/main/scala/utilities/Printer.scala b/src/main/scala/utilities/Printer.scala
index 7547ccc7d3a9d1105bf0214e8d87c3f15b5b7ac3..c65ae1e72a57e134b280ded4e9efb0455dc84610 100644
--- a/src/main/scala/utilities/Printer.scala
+++ b/src/main/scala/utilities/Printer.scala
@@ -346,8 +346,6 @@ object Printer {
})
}
- def prettySCProof(proof:SCProof): String = prettySCProof(SCValidProof(proof), false)
-
- // def prettyTheoryJudgement((proof: SCProof, judgement: SCProofCheckerJudgement = SCValidProof, forceDisplaySubproofs: Boolean = false))
+ def prettySCProof(proof: SCProof): String = prettySCProof(SCValidProof(proof), false)
}
diff --git a/src/main/scala/utilities/TheoriesHelpers.scala b/src/main/scala/utilities/TheoriesHelpers.scala
index fdab39b7e6e4558ae1d4f5cf16264b79843ed048..6c487530e98569f48f4cf4c028af0050909d7e1e 100644
--- a/src/main/scala/utilities/TheoriesHelpers.scala
+++ b/src/main/scala/utilities/TheoriesHelpers.scala
@@ -6,10 +6,25 @@ import lisa.kernel.proof.SequentCalculus.*
import lisa.kernel.proof.*
import utilities.Printer
+/**
+ * A helper file that provides various syntactic sugars for LISA's FOL and proofs. Best imported through utilities.Helpers
+ * Usage:
+ * <pre>
+ * import utilities.Helpers.*
+ * </pre>
+ * or
+ * <pre>
+ * extends utilities.KernelHelpers.*
+ * </pre>
+ */
trait TheoriesHelpers extends KernelHelpers {
- // for when the kernel will have a dedicated parser
- extension (theory: RunningTheory)
+ extension (theory: RunningTheory) {
+
+ /**
+ * Add a theorem to the theory, but also asks explicitely for the desired conclusion
+ * of the theorem to have more explicit writing and for sanity check.
+ */
def theorem(name: String, statement: String, proof: SCProof, justifications: Seq[theory.Justification]): RunningTheoryJudgement[theory.Theorem] = {
val expected = proof.conclusion // parse(statement)
if (expected == proof.conclusion) theory.makeTheorem(name, expected, proof, justifications)
@@ -17,19 +32,43 @@ trait TheoriesHelpers extends KernelHelpers {
else InvalidJustification("The proof does not prove the claimed statement", None)
}
- def functionDefinition(symbol:String, expression:LambdaTermFormula, out:VariableLabel, proof:SCProof, justifications:Seq[theory.Justification] ): RunningTheoryJudgement[theory.FunctionDefinition] = {
+ /**
+ * Make a function definition in the theory, but only ask for the identifier of the new symbol; Arity is inferred
+ * of the theorem to have more explicit writing and for sanity check. See [[lisa.kernel.proof.RunningTheory.makeFunctionDefinition]]
+ */
+ def functionDefinition(
+ symbol: String,
+ expression: LambdaTermFormula,
+ out: VariableLabel,
+ proof: SCProof,
+ justifications: Seq[theory.Justification]
+ ): RunningTheoryJudgement[theory.FunctionDefinition] = {
val label = ConstantFunctionLabel(symbol, expression.vars.size)
theory.makeFunctionDefinition(proof, justifications, label, out, expression)
}
- def predicateDefinition(symbol:String, expression:LambdaTermFormula): RunningTheoryJudgement[theory.PredicateDefinition] = {
+
+ /**
+ * Make a predicate definition in the theory, but only ask for the identifier of the new symbol; Arity is inferred
+ * of the theorem to have more explicit writing and for sanity check. See [[lisa.kernel.proof.RunningTheory.makePredicateDefinition]]
+ */
+ def predicateDefinition(symbol: String, expression: LambdaTermFormula): RunningTheoryJudgement[theory.PredicateDefinition] = {
val label = ConstantPredicateLabel(symbol, expression.vars.size)
theory.makePredicateDefinition(label, expression)
}
+ /**
+ * Try to fetch, in this order, a justification that is an Axiom with the given name,
+ * a Theorem with a given name or a Definition with a the given name as symbol
+ */
def getJustification(name: String): Option[theory.Justification] = theory.getAxiom(name).orElse(theory.getTheorem(name)).orElse(theory.getDefinition(name))
+ }
- extension (just: RunningTheory#Justification)
- def show(implicit output: String => Unit ): just.type = {
+ extension (just: RunningTheory#Justification) {
+
+ /**
+ * Outputs, with an implicit output function, a readable representation of the Axiom, Theorem or Definition.
+ */
+ def show(using output: String => Unit): just.type = {
just match
case thm: RunningTheory#Theorem => output(s" Theorem ${thm.name} := ${Printer.prettySequent(thm.proposition)}\n")
case axiom: RunningTheory#Axiom => output(s" Axiom ${axiom.name} := ${Printer.prettyFormula(axiom.ax)}\n")
@@ -38,18 +77,24 @@ trait TheoriesHelpers extends KernelHelpers {
case pd: RunningTheory#PredicateDefinition =>
output(s" Definition of predicate symbol ${pd.label.id} := ${Printer.prettyFormula(pd.label(pd.expression.vars.map(_())*) <=> pd.expression.body)}\n") // (label, args, phi)
case fd: RunningTheory#FunctionDefinition =>
- output(s" Definition of function symbol ${fd.label.id} := ${Printer.prettyFormula(( fd.out === fd.label(fd.expression.vars.map(_())*)) <=> fd.expression.body)})\n")
- // output(Printer.prettySequent(thm.proposition))
- // thm
+ output(s" Definition of function symbol ${Printer.prettyTerm(fd.label(fd.expression.vars.map(_())*))} := the ${fd.out.id} such that ${Printer
+ .prettyFormula((fd.out === fd.label(fd.expression.vars.map(_())*)) <=> fd.expression.body)})\n")
+ // output(Printer.prettySequent(thm.proposition))
+ // thm
just
}
+ }
extension [J <: RunningTheory#Justification](theoryJudgement: RunningTheoryJudgement[J]) {
- def showAndGet(output: String => Unit = println): J = {
+ /**
+ * If the Judgement is valid, show the inner justification and returns it.
+ * Otherwise, output the error leading to the invalid justification and throw an error.
+ */
+ def showAndGet(using output: String => Unit): J = {
theoryJudgement match
case RunningTheoryJudgement.ValidJustification(just) =>
- just.show(output)
+ just.show
case InvalidJustification(message, error) =>
output(s"$message\n${error match
case Some(judgement) => Printer.prettySCProof(judgement)
@@ -59,14 +104,12 @@ trait TheoriesHelpers extends KernelHelpers {
}
}
+ /**
+ * Output a readable representation of a proof.
+ */
def checkProof(proof: SCProof, output: String => Unit = println): Unit = {
val judgement = SCProofChecker.checkSCProof(proof)
output(Printer.prettySCProof(judgement))
}
-
-
-
-
-
}
diff --git a/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala b/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
deleted file mode 100644
index 36a3fb11e37022c4827d795d20d53fefddc173a2..0000000000000000000000000000000000000000
--- a/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
+++ /dev/null
@@ -1,90 +0,0 @@
-package lisa.proven
-
-import utilities.Printer
-import lisa.kernel.fol.FOL.*
-import lisa.kernel.fol.FOL.*
-import lisa.kernel.proof.SCProof
-import lisa.kernel.proof.SequentCalculus.Sequent
-import lisa.kernel.proof.SequentCalculus.*
-import lisa.settheory.AxiomaticSetTheory.*
-import proven.ElementsOfSetTheory.*
-import proven.tactics.ProofTactics
-import test.ProofCheckerSuite
-import utilities.Helpers.{_, given}
-import utilities.Helpers.{_, given}
-
-class ElementsOfSetTheoryTests extends ProofCheckerSuite {
-
- test("Verification of the proof of symmetry of the pair") {
- checkProof(proofUnorderedPairSymmetry, emptySeq +> forall(vl, forall(ul, pair(u, v) === pair(v, u))))
- }
-
- test("Verification of the proof of deconstruction of the unordered pair") {
- checkProof(
- proofUnorderedPairDeconstruction,
- emptySeq +>
- forall(
- sl,
- forall(
- tl,
- forall(
- ul,
- forall(
- vl,
- (pair(s, t) === pair(u, v)) ==>
- (((VariableTerm(v) === t) /\ (VariableTerm(u) === s)) \/ ((VariableTerm(s) === v) /\ (VariableTerm(t) === u)))
- )
- )
- )
- )
- )
- }
-
- // forall x, y. (x in {y, y}) <=> (x = y)
- val singletonSetEqualityProof: SCProof = {
- val t0 = SCSubproof(
- {
- val t0 = Rewrite(() |- pairAxiom, -1)
- val p0 = ProofTactics.instantiateForall(SCProof(IndexedSeq(t0), IndexedSeq(() |- pairAxiom)), t0.bot.right.head, v)
- val p1 = ProofTactics.instantiateForall(p0, p0.conclusion.right.head, v)
- val p2: SCProof = ProofTactics.instantiateForall(p1, p1.conclusion.right.head, u)
- p2
- },
- IndexedSeq(-1),
- display = false
- )
-
- // |- f <=> (f \/ f)
- def selfIffOr(f: Formula): SCSubproof = SCSubproof(
- {
- val t0 = Hypothesis(Sequent(Set(f), Set(f)), f)
- val t1 = RightOr(Sequent(Set(f), Set(f \/ f)), 0, f, f)
- val t2 = LeftOr(Sequent(Set(f \/ f), Set(f)), Seq(0, 0), Seq(f, f))
- val t3 = RightImplies(Sequent(Set(), Set(f ==> (f \/ f))), 1, f, f \/ f)
- val t4 = RightImplies(Sequent(Set(), Set((f \/ f) ==> f)), 2, f \/ f, f)
- val t5 = RightIff(Sequent(Set(), Set(f <=> (f \/ f))), 3, 4, f, f \/ f)
- SCProof(IndexedSeq(t0, t1, t2, t3, t4, t5))
- },
- display = false
- )
- val t1 = selfIffOr(u === v)
- val xy = u === v
- val h = SchematicPredicateLabel("h", 0)
- val t2 = RightSubstIff(
- Sequent(Set((xy \/ xy) <=> xy), Set(xy <=> in(u, pair(v, v)))),
- 0,
- List(((v === u) \/ (v === u), v === u)),
- LambdaFormulaFormula(Seq(h), in(u, pair(v, v)) <=> PredicateFormula(h, Seq.empty))
- )
- val t3 = Cut(Sequent(Set(), Set(xy <=> in(u, pair(v, v)))), 1, 2, (xy \/ xy) <=> xy)
-
- val p0 = SCProof(IndexedSeq(t0, t1, t2, t3), IndexedSeq(() |- pairAxiom))
-
- ProofTactics.generalizeToForall(ProofTactics.generalizeToForall(p0, vl), ul)
- }
-
- test("Singleton set equality") {
- checkProof(singletonSetEqualityProof, emptySeq +> forall(u, forall(v, (u === v) <=> in(u, pair(v, v)))))
- }
-
-}
diff --git a/src/test/scala/lisa/proven/InitialProofsTests.scala b/src/test/scala/lisa/proven/InitialProofsTests.scala
new file mode 100644
index 0000000000000000000000000000000000000000..331a3f44b312ca7015be8ce472d05ff4660f7c6d
--- /dev/null
+++ b/src/test/scala/lisa/proven/InitialProofsTests.scala
@@ -0,0 +1,20 @@
+package lisa.proven
+
+import utilities.Printer
+import test.ProofCheckerSuite
+
+class InitialProofsTests extends ProofCheckerSuite {
+ import proven.SetTheoryLibrary.*
+
+ test("File SetTheory initialize well") {
+ proven.mathematics.SetTheory
+ succeed
+ }
+
+ test("File Mapping initialize well") {
+ proven.mathematics.Mapping
+ succeed
+ }
+
+
+}