This theory formalizes minimal first-order logic [Benl et al., 1998], mFOL, in Nuprl
and defines provability and uniform evidence for for formulas of mFOL.
Our soundness/completness theorem for mFOL [Constable & Bickford, 2014] states that a formula of mFOL
is provable if and only if the type of uniform evidence for it is inhabited.
We are working on a formal Nuprl proof of this completeness theorem
but that will require some new primitive operations in the Nuprl computation system.
However, we can already prove the soundness direction of the theorem
as stated here: mFOL-proveable-formula-evidence.
Some explanation of the formal statement:
Formulas of mFOL are represented by members of the type ⌜mFOL()⌝.
That type and many operators on it are automatically generated from
CreateDataType
[ `atomic`: [ name, Atom
; vars, ℤ List
]
; `connect`: [ knd, Atom
; left, mFOL()
; right, mFOL()
]
; `quant`: [ isall, 𝔹
; var, ℤ
; body, mFOL()
]
]
In the atomic case, we are using integers, ℤ, to represent variables
and Atom (essentially tokens) for names of atomic relations.
Our language thus contains only relation symbols, and contains
countably many symbols of each arity.
Since in minimal logic there is no constant for False and no unary negation
connective, all the connectives are binary and we label those with a token
(a member of type Atom). In the proof system we define for mFOL(), only the tokens
"and", "or", and "imp" are relevant as connectives.
A quantified formula is a forall or exists formula depending on the boolean, isall.
Inductive definitions over mFOL() are made using the automatically generated
induction operator that is displayed as
⌜mFOL_ind(fmla;
mFOatomic(R,vars)⇒ [atomic];
mFOconnect(connective,a,b)⇒ reca,recb.[connect];
mFOquant(isall,x,body)⇒ rec.[quant]) ⌝
In order to define provability we must define the proof rules and
to do that we must define (among other things) equality of mFOL() formulas,
mFO-equal,
the free variables of a formula,
mFOL-freevars ,
and the bound variables of a formula,
mFOL-boundvars.
Since there are no function symbols in our language, we only need to
define substitution of one variable for another, but this still requires
renaming of bound variables (and this is why we chose to represent variables
as integers -- so that it is easy to generate fresh names).
Instead of defining alpha-equality of formulas, we define the
"abstract meaning" of a formula.
An abstract formula, AbstractFOFormula, assigns a meaning
(a member of ℙ, i.e. a type) to a domain, Dom, a structure over Dom,
and an assignment into Dom. A structure, FOStruct, over Dom,
assigns a meaning to each instance of an atomic formula.
An assignment, FOAssignment, assigns a member of Dom to each variable.
The meaning assigned by abstract formula phi to a given Dom, structure S,
and assignment a, FOSatWith, is displayed as ⌜Dom,S,a |= phi⌝ .
The abstract meaning of a mFOL() formula is defined inductively by
mFOL-abstract
Alpha-equal formulas define the same abstract formula.
So, to do renaming of bound variables
we prove a lemma mFOL-bound-rename that shows that there is a formula
with the same abstract meaning whose bound variables are disjoint from
a given list of variables.
Then we use the "extract" of that lemma as the renaming operator
mFOL-rename-bound-to-avoid
Now substitution, mFOL-subst,
is done by first renaming bound variables to
avoid the new variable and then renaming the old variable to the new varaible.
A sequent for mFOL, mFOL-sequent, is a list of hypothesis and a conclusion.
The abstract meaning of a sequent mFOL-sequent-abstract is a function
from the tuple of abstract meanings of the hypotheses to the abstract meaning
of the conclusion.
To define provablity for mFOL we create another data type ⌜mFOLRule()⌝ for the
rules of mFOL. It has eleven cases corresponding to the introduction and
elimination rules for "and", "or", "imp", "all", and "exists", plus the hypothesis
rule. It is not a recursive type, but the data-type package generates a case
operator for defining operations on rules, displayed as follows:
case(<rule>)
andI => <andI>
impI => <impI>
allI with <var> => <allI>
existsI with <v1> => <existsI>
orI (left?<left>) => <orI>
hyp => <hyp>
andE @<h1> => <andE>
orE @<h2> => <orE>
impE @<h3> => <impE>
allE @<h4> with <v2> => <allE>
existsE @<h5> with <v3> => <existsE>
Now we can define the effect of a given rule on a given mFOL sequent.
If the rule does not apply, then it `fails` by producing the effect ⌜inr ⋅ ⌝
otherwise it succeeds and produces ⌜inl L⌝ where L is the list of subgoal sequents.
Here is the definition:
mFOLeffect
Using this we define provability: mFOL-proveable
making use of a generic definition of provability, proveable.
It says that a sequent is provable if there is a correct proof tree.
A proof tree proof-tree is a well-founded tree
(for those we use Martin-Lof's, W type, W)
with a sequent and a rule labeling each node.
The proof is correct for sequent s if the sequent labeling the top node is s
and for every node, the effect of the given rule on the given sequent
does not fail and the successors of the node
are correct proofs of the generated subgoal sequents.
Since proof trees are well-founded, we may prove properties of them by induction,
and we do that to prove the main soundness therorem
mFOL-proveable-evidence
It says that from a correct proof of a mFOL sequent we may construct
uniform evidence mFOL-sequent-evidence for the sequent.
Uniform evidence for an abstract formula, fmla, is the
intersection over all domains, Dom, and all structures, S, over Dom,
of evidence for ∀a:FOAssignment(vs,Dom). Dom,S,a |= fmla
where vs is the list of free variables of the formula.
NOTE:
If the formula is closed (i.e. the free vars is the nil list) then
an assignment a:FOAssignment([],Dom) exists even when Dom is an empty type..
Thus, (forall x. P(x)) => (exists x. P(x)) is not uniformly valid
because the premise is true for an empty domain while the conclusion is not.
By the soundness theorem, it is not provable.
By examining the effect of the mFOL rules
(see mFOLeffect)
one can see why this is so:
both forall elimination and exists introduction
can only be used with a variable already free in the sequent,
so there is no way to use either rule in a proof of this formula.
The proof of the main soundness theorem is by induction on the correct proof tree
and reduces to twelve cases (one for each of the eleven rules except orI
which generates two cases).
The case for the hypothesis rule follows from this lemma: mFOL-sequent-evidence-trivial.
The propositional cases are fairly straightforward, using these lemmas:
mFOL-sequent-evidence_transitivity1,
mFOL-sequent-evidence_transitivity2,
and mFOL-sequent-evidence_and.
The quantifier cases, for allI, allE, existsI, existsE are trickier
but follow essentially from mFOL-subst-abstract.
⋅
Definition: ex-approx
ex-approx(e;t;t') == ∀f:Base. (e#f:Base ⇒ (f t?e:v.⊥ ≤ f t'?e:v.⊥))
Lemma: ex-approx_wf
∀[e:Atom2]. ∀[t,t':Base]. (ex-approx(e;t;t') ∈ ℙ)
Lemma: sq_stable__ex-approx
∀[e:Atom2]. ∀[t,t':Base]. SqStable(ex-approx(e;t;t'))
Lemma: ex-approx_transitivity
∀[e:Atom2]. ∀[t1,t2,t3:Base]. (ex-approx(e;t1;t3)) supposing (ex-approx(e;t1;t2) and ex-approx(e;t2;t3))
Lemma: ex-approx-context
∀[e:Atom2]. ∀[a,b,g:Base]. (ex-approx(e;g a;g b)) supposing (ex-approx(e;a;b) and e#g:Base)
Definition: FOAssignment
An assignment assigns a member of Dom to each variable.
(Variables in mFOL() formulas are represented by integers).⋅
FOAssignment(vs,Dom) == {z:ℤ| (z ∈ vs)} ⟶ Dom
Lemma: FOAssignment_wf
∀[vs:ℤ List]. ∀[Dom:Type]. (FOAssignment(vs,Dom) ∈ Type)
Lemma: subtype_rel_FOAssignment
∀[vs1,vs2:ℤ List]. ∀[Dom:Type]. FOAssignment(vs1,Dom) ⊆r FOAssignment(vs2,Dom) supposing vs2 ⊆ vs1
Definition: FOStruct
A structure over Dom,
assigns a meaning to each instance of an atomic formula.⋅
FOStruct(Dom) == Atom ⟶ (Dom List) ⟶ ℙ
Lemma: FOStruct_wf
∀[Dom:Type]. (FOStruct(Dom) ∈ 𝕌')
Definition: FOStruct+
FOStruct+{i:l}(Dom) == {S:FOStruct(Dom)| exception-type(S "false" [])}
Lemma: FOStruct+_wf
∀[Dom:Type]. (FOStruct+{i:l}(Dom) ∈ 𝕌')
Definition: update-assignment
a[x := v] == λz.if (z =z x) then v else a z fi
Lemma: update-assignment_wf
∀[vs:ℤ List]. ∀[z:ℤ]. ∀[Dom:Type]. ∀[a:FOAssignment(filter(λx.(¬b(x =z z));vs),Dom)]. ∀[v:Dom].
(a[z := v] ∈ FOAssignment(vs,Dom))
Definition: AbstractFOFormula
AbstractFOFormula(vs) == Dom:Type ⟶ S:FOStruct(Dom) ⟶ FOAssignment(vs,Dom) ⟶ ℙ
Lemma: AbstractFOFormula_wf
∀[vs:ℤ List]. (AbstractFOFormula(vs) ∈ 𝕌')
Definition: AbstractFOFormula+
AbstractFOFormula+(vs) == Dom:Type ⟶ S:FOStruct+{i:l}(Dom) ⟶ FOAssignment(vs,Dom) ⟶ ℙ
Lemma: AbstractFOFormula+_wf
∀[vs:ℤ List]. (AbstractFOFormula+(vs) ∈ 𝕌')
Definition: FOSatWith
An abstract formula is a function that assigns a meaning (a proposition)
to a given Dom, structure S, and assignment a. So, this definition is mainly
for notation.⋅
Dom,S,a |= fmla == fmla Dom S a
Lemma: FOSatWith_wf
∀[vs:ℤ List]. ∀[Dom:Type]. ∀[S:FOStruct(Dom)]. ∀[a:FOAssignment(vs,Dom)]. ∀[fmla:AbstractFOFormula(vs)].
(Dom,S,a |= fmla ∈ ℙ)
Definition: FOSatWith+
Dom,S,a +|= fmla == fmla Dom S a
Lemma: FOSatWith+_wf
∀[vs:ℤ List]. ∀[Dom:Type]. ∀[S:FOStruct+{i:l}(Dom)]. ∀[a:FOAssignment(vs,Dom)]. ∀[fmla:AbstractFOFormula+(vs)].
(Dom,S,a +|= fmla ∈ ℙ)
Definition: mFO-uniform-evidence
An abstract formula fmla with free variables, vs, is true
given domain Dom and structure S over Dom
if it is true for any assignment into Dom of its free variables.
Evidence for that is given by the proposition (type)
∀a:FOAssignment(vs,Dom). Dom,S,a |= fmla
Uniform evidence for an abstract formula, fmla, is the
intersection over all domains, Dom, and all structures, S, over Dom,
of that evidence.⋅
mFO-uniform-evidence(vs;fmla) == ⋂Dom:Type. ⋂S:FOStruct(Dom). ∀a:FOAssignment(vs,Dom). Dom,S,a |= fmla
Lemma: mFO-uniform-evidence_wf
∀[vs:ℤ List]. ∀[fmla:AbstractFOFormula(vs)]. (mFO-uniform-evidence(vs;fmla) ∈ 𝕌')
Definition: mFO_uniform_evidence
mFO_uniform_evidence{i:l}(fmla) == ⋂Dom:Type. ⋂S:FOStruct(Dom). ∀a:ℤ ⟶ Dom. Dom,S,a |= fmla
Lemma: mFO_uniform_evidence_wf
∀[vs:ℤ List]. ∀[fmla:AbstractFOFormula(vs)]. (mFO_uniform_evidence{i:l}(fmla) ∈ 𝕌')
Definition: FO-uniform-evidence
FO-uniform-evidence(vs;fmla) == ⋂Dom:Type. ⋂S:FOStruct+{i:l}(Dom). ∀a:FOAssignment(vs,Dom). Dom,S,a +|= fmla
Lemma: FO-uniform-evidence_wf
∀[vs:ℤ List]. ∀[fmla:AbstractFOFormula+(vs)]. (FO-uniform-evidence(vs;fmla) ∈ 𝕌')
Definition: AbstractFOAtomic
If S is a structure (for a domain Dom), then ⌜S n ∈ (Dom List) ⟶ ℙ⌝.
If a is an assignment on Dom, then ⌜map(a;L) ∈ Dom List⌝. Thus, the
meaning of the atomic formula ⌜n(L)⌝
(which is predicate symbol ⌜n ∈ Atom⌝ applied to variable list ⌜L ∈ ℤ List⌝)
is S n map(a;L)⋅
AbstractFOAtomic(n;L) == λDom,S,a. (S n map(a;L))
Lemma: AbstractFOAtomic_wf
∀[n:Atom]. ∀[L:ℤ List]. (AbstractFOAtomic(n;L) ∈ AbstractFOFormula(L))
Definition: AbstractFOAtomic+
AbstractFOAtomic+(n;L) == λDom,S,a. ((S n map(a;L)) ⋃ (S "false" []))
Lemma: AbstractFOAtomic+_wf
∀[n:Atom]. ∀[L:ℤ List]. (AbstractFOAtomic+(n;L) ∈ AbstractFOFormula+(L))
Definition: FOConnective
FOConnective(knd) ==
λx,y,Dom,S,a. let p = Dom,S,a |= x in
let q = Dom,S,a |= y in
if knd =a "and" then p ∧ q
if knd =a "or" then p ∨ q
else p ⇒ q
fi
Lemma: FOConnective_wf
∀[vsa,vsb:ℤ List].
∀knd:Atom
(FOConnective(knd) ∈ AbstractFOFormula(vsa)
⟶ AbstractFOFormula(vsb)
⟶ AbstractFOFormula(val-union(IntDeq;vsa;vsb)))
Definition: FOConnective+
FOConnective+(knd) ==
λx,y,Dom,S,a. let p = Dom,S,a +|= x in
let q = Dom,S,a +|= y in
if knd =a "and" then (p ∧ q) ⋃ (S "false" [])
if knd =a "or" then (p ∨ q) ⋃ (S "false" [])
else (p ⇒ q) ⋃ (S "false" [])
fi
Lemma: FOConnective+_wf
∀[vsa,vsb:ℤ List].
∀knd:Atom
(FOConnective+(knd) ∈ AbstractFOFormula+(vsa)
⟶ AbstractFOFormula+(vsb)
⟶ AbstractFOFormula+(val-union(IntDeq;vsa;vsb)))
Definition: FOQuantifier
FOQuantifier(isall) ==
λx,fmla,Dom,S,a. if isall then ∀v:Dom. Dom,S,a[x := v] |= fmla else ∃v:Dom. Dom,S,a[x := v] |= fmla fi
Lemma: FOQuantifier_wf
∀[vs:ℤ List]. ∀[isall:𝔹].
(FOQuantifier(isall) ∈ z:ℤ ⟶ AbstractFOFormula(vs) ⟶ AbstractFOFormula(filter(λx.(¬b(x =z z));vs)))
Definition: FOQuantifier+
FOQuantifier+(isall) ==
λx,fmla,Dom,S,a. if isall
then (∀v:Dom. Dom,S,a[x := v] +|= fmla) ⋃ (S "false" [])
else (∃v:Dom. Dom,S,a[x := v] +|= fmla) ⋃ (S "false" [])
fi
Lemma: FOQuantifier+_wf
∀[vs:ℤ List]. ∀[isall:𝔹].
(FOQuantifier+(isall) ∈ z:ℤ ⟶ AbstractFOFormula+(vs) ⟶ AbstractFOFormula+(filter(λx.(¬b(x =z z));vs)))
Definition: mFOLco
mFOLco() ==
corec(X.lbl:Atom × if lbl =a "atomic" then name:Atom × (ℤ List)
if lbl =a "connect" then knd:Atom × left:X × X
if lbl =a "quant" then isall:𝔹 × var:ℤ × X
else Void
fi )
Lemma: mFOLco_wf
mFOLco() ∈ Type
Lemma: mFOLco-ext
mFOLco() ≡ lbl:Atom × if lbl =a "atomic" then name:Atom × (ℤ List)
if lbl =a "connect" then knd:Atom × left:mFOLco() × mFOLco()
if lbl =a "quant" then isall:𝔹 × var:ℤ × mFOLco()
else Void
fi
Definition: mFOLco_size
mFOLco_size(p) ==
fix((λsize,p. let lbl,x = p
in if lbl =a "atomic" then 0
if lbl =a "connect" then let knd,left,z = x in (1 + (size left)) + (size z)
if lbl =a "quant" then let isall,var,z = x in 1 + (size z)
else 0
fi ))
p
Lemma: mFOLco_size_wf
∀[p:mFOLco()]. (mFOLco_size(p) ∈ partial(ℕ))
Definition: mFOL
mFOL() == {p:mFOLco()| (mFOLco_size(p))↓}
Lemma: mFOL_wf
mFOL() ∈ Type
Definition: mFOL_size
mFOL_size(p) ==
fix((λsize,p. let lbl,x = p
in if lbl =a "atomic" then 0
if lbl =a "connect" then let knd,left,z = x in (1 + (size left)) + (size z)
if lbl =a "quant" then let isall,var,z = x in 1 + (size z)
else 0
fi ))
p
Lemma: mFOL_size_wf
∀[p:mFOL()]. (mFOL_size(p) ∈ ℕ)
Lemma: mFOL-ext
mFOL() ≡ lbl:Atom × if lbl =a "atomic" then name:Atom × (ℤ List)
if lbl =a "connect" then knd:Atom × left:mFOL() × mFOL()
if lbl =a "quant" then isall:𝔹 × var:ℤ × mFOL()
else Void
fi
Definition: mFOatomic
name(vars) == <"atomic", name, vars>
Lemma: mFOatomic_wf
∀[name:Atom]. ∀[vars:ℤ List]. (name(vars) ∈ mFOL())
Definition: mFOconnect
mFOconnect(knd;left;right) == <"connect", knd, left, right>
Lemma: mFOconnect_wf
∀[knd:Atom]. ∀[left,right:mFOL()]. (mFOconnect(knd;left;right) ∈ mFOL())
Definition: mFOquant
mFOquant(isall;var;body) == <"quant", isall, var, body>
Lemma: mFOquant_wf
∀[isall:𝔹]. ∀[var:ℤ]. ∀[body:mFOL()]. (mFOquant(isall;var;body) ∈ mFOL())
Definition: mFOatomic?
mFOatomic?(v) == fst(v) =a "atomic"
Lemma: mFOatomic?_wf
∀[v:mFOL()]. (mFOatomic?(v) ∈ 𝔹)
Definition: mFOatomic-name
mFOatomic-name(v) == fst(snd(v))
Lemma: mFOatomic-name_wf
∀[v:mFOL()]. mFOatomic-name(v) ∈ Atom supposing ↑mFOatomic?(v)
Definition: mFOatomic-vars
mFOatomic-vars(v) == snd(snd(v))
Lemma: mFOatomic-vars_wf
∀[v:mFOL()]. mFOatomic-vars(v) ∈ ℤ List supposing ↑mFOatomic?(v)
Definition: mFOconnect?
mFOconnect?(v) == fst(v) =a "connect"
Lemma: mFOconnect?_wf
∀[v:mFOL()]. (mFOconnect?(v) ∈ 𝔹)
Definition: mFOconnect-knd
mFOconnect-knd(v) == fst(snd(v))
Lemma: mFOconnect-knd_wf
∀[v:mFOL()]. mFOconnect-knd(v) ∈ Atom supposing ↑mFOconnect?(v)
Definition: mFOconnect-left
mFOconnect-left(v) == fst(snd(snd(v)))
Lemma: mFOconnect-left_wf
∀[v:mFOL()]. mFOconnect-left(v) ∈ mFOL() supposing ↑mFOconnect?(v)
Definition: mFOconnect-right
mFOconnect-right(v) == snd(snd(snd(v)))
Lemma: mFOconnect-right_wf
∀[v:mFOL()]. mFOconnect-right(v) ∈ mFOL() supposing ↑mFOconnect?(v)
Definition: mFOquant?
mFOquant?(v) == fst(v) =a "quant"
Lemma: mFOquant?_wf
∀[v:mFOL()]. (mFOquant?(v) ∈ 𝔹)
Definition: mFOquant-isall
mFOquant-isall(v) == fst(snd(v))
Lemma: mFOquant-isall_wf
∀[v:mFOL()]. mFOquant-isall(v) ∈ 𝔹 supposing ↑mFOquant?(v)
Definition: mFOquant-var
mFOquant-var(v) == fst(snd(snd(v)))
Lemma: mFOquant-var_wf
∀[v:mFOL()]. mFOquant-var(v) ∈ ℤ supposing ↑mFOquant?(v)
Definition: mFOquant-body
mFOquant-body(v) == snd(snd(snd(v)))
Lemma: mFOquant-body_wf
∀[v:mFOL()]. mFOquant-body(v) ∈ mFOL() supposing ↑mFOquant?(v)
Lemma: mFOL-induction
∀[P:mFOL() ⟶ ℙ]
((∀name:Atom. ∀vars:ℤ List. P[name(vars)])
⇒ (∀knd:Atom. ∀left,right:mFOL(). (P[left] ⇒ P[right] ⇒ P[mFOconnect(knd;left;right)]))
⇒ (∀isall:𝔹. ∀var:ℤ. ∀body:mFOL(). (P[body] ⇒ P[mFOquant(isall;var;body)]))
⇒ {∀v:mFOL(). P[v]})
Lemma: mFOL-definition
∀[A:Type]. ∀[R:A ⟶ mFOL() ⟶ ℙ].
((∀name:Atom. ∀vars:ℤ List. {x:A| R[x;name(vars)]} )
⇒ (∀knd:Atom. ∀left,right:mFOL(). ({x:A| R[x;left]} ⇒ {x:A| R[x;right]} ⇒ {x:A| R[x;mFOconnect(knd;left;right)]}\000C ))
⇒ (∀isall:𝔹. ∀var:ℤ. ∀body:mFOL(). ({x:A| R[x;body]} ⇒ {x:A| R[x;mFOquant(isall;var;body)]} ))
⇒ {∀v:mFOL(). {x:A| R[x;v]} })
Definition: mFOL_ind
mFOL_ind(v;
mFOatomic(name,vars)⇒ atomic[name; vars];
mFOconnect(knd,left,right)⇒ rec1,rec2.connect[knd;
left;
right;
rec1;
rec2];
mFOquant(isall,var,body)⇒ rec3.quant[isall;
var;
body;
rec3]) ==
fix((λmFOL_ind,v. let lbl,v1 = v
in if lbl="atomic" then let name,v2 = v1 in atomic[name; v2]
if lbl="connect"
then let knd,v2 = v1
in let left,v3 = v2
in connect[knd;
left;
v3;
mFOL_ind left;
mFOL_ind v3]
if lbl="quant"
then let isall,v2 = v1
in let var,v3 = v2
in quant[isall;
var;
v3;
mFOL_ind v3]
else Ax
fi ))
v
Lemma: mFOL_ind_wf
∀[A:Type]. ∀[R:A ⟶ mFOL() ⟶ ℙ]. ∀[v:mFOL()]. ∀[atomic:name:Atom ⟶ vars:(ℤ List) ⟶ {x:A| R[x;name(vars)]} ].
∀[connect:knd:Atom
⟶ left:mFOL()
⟶ right:mFOL()
⟶ {x:A| R[x;left]}
⟶ {x:A| R[x;right]}
⟶ {x:A| R[x;mFOconnect(knd;left;right)]} ]. ∀[quant:isall:𝔹
⟶ var:ℤ
⟶ body:mFOL()
⟶ {x:A| R[x;body]}
⟶ {x:A| R[x;mFOquant(isall;var;body)]} ].
(mFOL_ind(v;
mFOatomic(name,vars)⇒ atomic[name;vars];
mFOconnect(knd,left,right)⇒ rec1,rec2.connect[knd;left;right;rec1;rec2];
mFOquant(isall,var,body)⇒ rec3.quant[isall;var;body;rec3]) ∈ {x:A| R[x;v]} )
Lemma: mFOL_ind_wf_simple
∀[A:Type]. ∀[v:mFOL()]. ∀[atomic:name:Atom ⟶ vars:(ℤ List) ⟶ A]. ∀[connect:knd:Atom
⟶ left:mFOL()
⟶ right:mFOL()
⟶ A
⟶ A
⟶ A]. ∀[quant:isall:𝔹
⟶ var:ℤ
⟶ body:mFOL()
⟶ A
⟶ A].
(mFOL_ind(v;
mFOatomic(name,vars)⇒ atomic[name;vars];
mFOconnect(knd,left,right)⇒ rec1,rec2.connect[knd;left;right;rec1;rec2];
mFOquant(isall,var,body)⇒ rec3.quant[isall;var;body;rec3]) ∈ A)
Definition: mFOLvar
vn == n
Lemma: mFOLvar_wf
∀[n:ℤ]. (vn ∈ ℤ)
Definition: mFOL_case
case(fmla)
P(vars) => atomic[P; vars];
A knd B => connect[knd;
A;
B];
isall v.body => quant[isall;
v;
body] ==
if mFOatomic?(fmla) then atomic[mFOatomic-name(fmla); mFOatomic-vars(fmla)]
if mFOconnect?(fmla)
then connect[mFOconnect-knd(fmla);
mFOconnect-left(fmla);
mFOconnect-right(fmla)]
else quant[mFOquant-isall(fmla);
mFOquant-var(fmla);
mFOquant-body(fmla)]
fi
Lemma: mFOL_case_wf
∀[T:Type]. ∀[v:mFOL()]. ∀[atomic:name:Atom ⟶ vars:(ℤ List) ⟶ T]. ∀[connect:knd:Atom
⟶ left:mFOL()
⟶ right:mFOL()
⟶ T]. ∀[quant:isall:𝔹
⟶ var:ℤ
⟶ body:mFOL()
⟶ T].
(case(v)
name(vars) => atomic[name;vars];
left knd right => connect[knd;left;right];
isall var.body => quant[isall;var;body] ∈ T)
Definition: nobrackets
(nobrackets):: l == l
Definition: mFO-dest-atomic
let a,b = dest-atomic(fmla) in
F[a; b] ==
if mFOatomic?(fmla) then F[mFOatomic-name(fmla); mFOatomic-vars(fmla)] else inr ⋅ fi
Lemma: mFO-dest-atomic_wf
∀[T:Type]. ∀[F:Atom ⟶ (ℤ List) ⟶ (T?)]. ∀[fmla:mFOL()]. (let nm,vars = dest-atomic(fmla) inF[nm;vars] ∈ T?)
Definition: mFO-dest-connective
let a,b = dest-knd(fmla) in
F[a; b] ==
if mFOconnect?(fmla) ∧b mFOconnect-knd(fmla) =a knd
then F[mFOconnect-left(fmla); mFOconnect-right(fmla)]
else inr ⋅
fi
Lemma: mFO-dest-connective_wf
∀[T:Type]. ∀[F:mFOL() ⟶ mFOL() ⟶ (T?)]. ∀[fmla:mFOL()]. ∀[knd:Atom]. (let a,b = dest-knd(fmla) in F[a;b] ∈ T?)
Definition: mFO-dest-quantifier
let v,b = dest-if isall then all else exists(fmla); in
F[v; b] ==
if mFOquant?(fmla) ∧b mFOquant-isall(fmla) =b isall then F[mFOquant-var(fmla); mFOquant-body(fmla)] else inr ⋅ fi
Lemma: mFO-dest-quantifier_wf
∀[T:Type]. ∀[F:ℤ ⟶ mFOL() ⟶ (T?)]. ∀[fmla:mFOL()]. ∀[isall:𝔹].
(let v,b = dest-if isall then all else exists(fmla); in
F[v;b] ∈ T?)
Definition: mFO-equal
mFO-equal(x) ==
mFOL_ind(x;
mFOatomic(R,vars)⇒ λy.let R',vars' = dest-atomic(y) in
R =a R' ∧b (list-deq(IntDeq) vars vars');
mFOconnect(knd,a,b)⇒ eqa,eqb.λy.let a',b' = dest-knd(y) in
(eqa a') ∧b (eqb b');
mFOquant(isall,v,b)⇒ eqb.λy.let w,b' = dest-if isall then all else exists(y); in
(v =z w) ∧b (eqb b'))
Lemma: mFO-equal_wf
∀[x:mFOL()]. (mFO-equal(x) ∈ mFOL() ⟶ 𝔹)
Definition: eq_mFO
eq_mFO(x;y) == mFO-equal(x) y
Lemma: eq_mFO_wf
∀[x,y:mFOL()]. (eq_mFO(x;y) ∈ 𝔹)
Lemma: assert-eq_mFO
∀[x,y:mFOL()]. uiff(↑eq_mFO(x;y);x = y ∈ mFOL())
Definition: deq-mFO
deq-mFO() == λx,y. eq_mFO(x;y)
Lemma: deq-mFO_wf
deq-mFO() ∈ EqDecider(mFOL())
Definition: mFOL-freevars
mFOL-freevars(fmla) ==
mFOL_ind(fmla;
mFOatomic(R,vars)⇒ remove-repeats(IntDeq;vars);
mFOconnect(knd,a,b)⇒ fvsa,fvsb.val-union(IntDeq;fvsa;fvsb);
mFOquant(isall,z,body)⇒ fvsbody.filter(λx.(¬b(x =z z));fvsbody))
Lemma: mFOL-freevars_wf
∀[fmla:mFOL()]. (mFOL-freevars(fmla) ∈ ℤ List)
Lemma: mFOL-freevars-connect-left-contained
∀fmla:mFOL(). mFOL-freevars(mFOconnect-left(fmla)) ⊆ mFOL-freevars(fmla) supposing ↑mFOconnect?(fmla)
Lemma: mFOL-freevars-connect-right-contained
∀fmla:mFOL(). mFOL-freevars(mFOconnect-right(fmla)) ⊆ mFOL-freevars(fmla) supposing ↑mFOconnect?(fmla)
Lemma: mFOL-freevars-connect-contained
∀x,y:mFOL(). ∀knd:Atom. ∀vs:ℤ List.
((mFOL-freevars(x) ⊆ vs ∧ mFOL-freevars(y) ⊆ vs) ⇒ mFOL-freevars(mFOconnect(knd;x;y)) ⊆ vs)
Definition: mFOL-boundvars
mFOL-boundvars(fmla) ==
mFOL_ind(fmla;
mFOatomic(R,vars)⇒ [];
mFOconnect(knd,a,b)⇒ bvsa,bvsb.bvsa ⋃ bvsb;
mFOquant(isall,z,body)⇒ bvsbody.insert(z;bvsbody))
Lemma: mFOL-boundvars_wf
∀[fmla:mFOL()]. (mFOL-boundvars(fmla) ∈ ℤ List)
Definition: mFOL-rename
mFOL-rename(fmla;old;new) ==
mFOL_ind(fmla;
mFOatomic(R,vars)⇒ R(map(λv.if (v =z old) then new else v fi ;vars));
mFOconnect(knd,a,b)⇒ a',b'.mFOconnect(knd;a';b');
mFOquant(isall,x,body)⇒ body'.mFOquant(isall;x;if (x =z old) then body else body' fi ))
Lemma: mFOL-rename_wf
∀[fmla:mFOL()]. ∀[old,new:ℤ]. (mFOL-rename(fmla;old;new) ∈ mFOL())
Lemma: trivial-mFOL-rename
∀x,y:ℤ. ∀fmla:mFOL(). ((¬(y ∈ mFOL-freevars(fmla))) ⇒ (fmla = mFOL-rename(fmla;y;x) ∈ mFOL()))
Lemma: mFOL-boundvars-of-rename
∀[fmla:mFOL()]. ∀[old,new:ℤ]. (mFOL-boundvars(mFOL-rename(fmla;old;new)) = mFOL-boundvars(fmla) ∈ (ℤ List))
Lemma: mFOL-freevars-of-rename
∀fmla:mFOL(). ∀old,new:ℤ.
∀x:ℤ
((x ∈ mFOL-freevars(mFOL-rename(fmla;old;new)))
⇐⇒ ((¬(x = old ∈ ℤ)) ∧ (x ∈ mFOL-freevars(fmla))) ∨ ((x = new ∈ ℤ) ∧ (old ∈ mFOL-freevars(fmla))))
supposing ¬(new ∈ mFOL-boundvars(fmla))
Lemma: filter-mFOL-freevars-of-rename
∀z,z':ℤ. ∀fmla':mFOL().
((¬(z' ∈ mFOL-boundvars(fmla')))
⇒ (¬(z' ∈ mFOL-freevars(fmla')))
⇒ (filter(λx.(¬b(x =z z'));mFOL-freevars(mFOL-rename(fmla';z;z')))
= filter(λx.(¬b(x =z z));mFOL-freevars(fmla'))
∈ (ℤ List)))
Definition: mFOL-abstract
The abstract meaning of a mFOL() formula defined inductively.
Alpha-equal formulas define the same abstract formula.⋅
mFOL-abstract(fmla) ==
mFOL_ind(fmla;
mFOatomic(R,vars)⇒ AbstractFOAtomic(R;vars);
mFOconnect(knd,a,b)⇒ r1,r2.FOConnective(knd) r1 r2;
mFOquant(isall,x,body)⇒ r.FOQuantifier(isall) x r)
Lemma: mFOL-abstract_wf
∀[fmla:mFOL()]. (mFOL-abstract(fmla) ∈ AbstractFOFormula(mFOL-freevars(fmla)))
Lemma: mFOL-abstract-has-value
∀[fmla:mFOL()]. (mFOL-abstract(fmla))↓
Definition: FOAssigment-rename
FOAssigment-rename(a;fmla;x;y) == if y ∈b mFOL-freevars(fmla) then a[y := a x] else a fi
Lemma: FOAssigment-rename_wf
∀[Dom:Type]. ∀[x,y:ℤ]. ∀[fmla:mFOL()]. ∀[a:FOAssignment(mFOL-freevars(mFOL-rename(fmla;y;x)),Dom)].
FOAssigment-rename(a;fmla;x;y) ∈ FOAssignment(mFOL-freevars(fmla),Dom) supposing ¬(x ∈ mFOL-boundvars(fmla))
Lemma: mFOL-abstract-rename
∀[Dom:Type]. ∀[S:FOStruct(Dom)].
∀x,y:ℤ. ∀fmla:mFOL().
((¬(x ∈ mFOL-boundvars(fmla)))
⇒ (∀a1:FOAssignment(mFOL-freevars(mFOL-rename(fmla;y;x)),Dom). ∀a2:FOAssignment(mFOL-freevars(fmla),Dom).
((a2 = FOAssigment-rename(a1;fmla;x;y) ∈ FOAssignment(mFOL-freevars(fmla),Dom))
⇒ (Dom,S,a2 |= mFOL-abstract(fmla) = Dom,S,a1 |= mFOL-abstract(mFOL-rename(fmla;y;x)) ∈ ℙ))))
Definition: FOL-abstract
FOL-abstract(fmla) ==
mFOL_ind(fmla;
mFOatomic(R,vars)⇒ AbstractFOAtomic+(R;vars);
mFOconnect(knd,a,b)⇒ r1,r2.FOConnective+(knd) r1 r2;
mFOquant(isall,x,body)⇒ r.FOQuantifier+(isall) x r)
Lemma: FOL-abstract_wf
∀[fmla:mFOL()]. (FOL-abstract(fmla) ∈ AbstractFOFormula+(mFOL-freevars(fmla)))
Lemma: FOL-abstract-rename
∀[Dom:Type]. ∀[S:FOStruct+{i:l}(Dom)].
∀x,y:ℤ. ∀fmla:mFOL().
((¬(x ∈ mFOL-boundvars(fmla)))
⇒ (∀a1:FOAssignment(mFOL-freevars(mFOL-rename(fmla;y;x)),Dom). ∀a2:FOAssignment(mFOL-freevars(fmla),Dom).
((a2 = FOAssigment-rename(a1;fmla;x;y) ∈ FOAssignment(mFOL-freevars(fmla),Dom))
⇒ (Dom,S,a2 +|= FOL-abstract(fmla) = Dom,S,a1 +|= FOL-abstract(mFOL-rename(fmla;y;x)) ∈ ℙ))))
Lemma: mFOL-bound-rename
This lemma shows that there is a formula
with the same abstract meaning whose bound variables are disjoint from
a given list of variables.⋅
∀fmla:mFOL(). ∀L:ℤ List.
(∃fmla':mFOL() [((mFOL-freevars(fmla') = mFOL-freevars(fmla) ∈ (ℤ List))
∧ (mFOL-abstract(fmla') = mFOL-abstract(fmla) ∈ AbstractFOFormula(mFOL-freevars(fmla)))
∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))])
Lemma: FOL-bound-rename
This lemma shows that there is a formula
with the same abstract meaning whose bound variables are disjoint from
a given list of variables.⋅
∀fmla:mFOL(). ∀L:ℤ List.
(∃fmla':mFOL() [((mFOL-freevars(fmla') = mFOL-freevars(fmla) ∈ (ℤ List))
∧ (FOL-abstract(fmla') = FOL-abstract(fmla) ∈ AbstractFOFormula+(mFOL-freevars(fmla)))
∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))])
Definition: mFOL-rename-bound-to-avoid
A renaming operator on mFOL() formulas.
It renames the bound variables to be disjoint from the given list
and produces a formula (alpha-equivalent) with the same abstract meaning.⋅
mFOL-rename-bound-to-avoid(fmla;L) == TERMOF{mFOL-bound-rename:o, 1:l, 1:l} fmla L
Lemma: mFOL-rename-bound-to-avoid_wf
∀fmla:mFOL(). ∀L:ℤ List.
(mFOL-rename-bound-to-avoid(fmla;L) ∈ {fmla':mFOL()|
(mFOL-freevars(fmla') = mFOL-freevars(fmla) ∈ (ℤ List))
∧ (mFOL-abstract(fmla')
= mFOL-abstract(fmla)
∈ AbstractFOFormula(mFOL-freevars(fmla)))
∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla'))} )
Definition: FOL-rename-bound-to-avoid
FOL-rename-bound-to-avoid(fmla;L) == TERMOF{FOL-bound-rename:o, 1:l, 1:l} fmla L
Lemma: FOL-rename-bound-to-avoid_wf
∀fmla:mFOL(). ∀L:ℤ List.
(FOL-rename-bound-to-avoid(fmla;L) ∈ {fmla':mFOL()|
(mFOL-freevars(fmla') = mFOL-freevars(fmla) ∈ (ℤ List))
∧ (FOL-abstract(fmla')
= FOL-abstract(fmla)
∈ AbstractFOFormula+(mFOL-freevars(fmla)))
∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla'))} )
Definition: mFOL-subst
Substitute variable nw for variable old in fmla.
To do that, first rename the bound variables to avoid nw
and then rename old to nw.⋅
fmla[nw/old] == mFOL-rename(mFOL-rename-bound-to-avoid(fmla;[nw]);old;nw)
Lemma: mFOL-subst_wf
∀[fmla:mFOL()]. ∀[nw,old:ℤ]. (fmla[nw/old] ∈ mFOL())
Lemma: freevars-mFOL-subst
∀fmla:mFOL(). ∀nw,old,x:ℤ.
((x ∈ mFOL-freevars(fmla[nw/old]))
⇐⇒ ((¬(x = old ∈ ℤ)) ∧ (x ∈ mFOL-freevars(fmla))) ∨ ((x = nw ∈ ℤ) ∧ (old ∈ mFOL-freevars(fmla))))
Lemma: mFOL-subst-trivial
∀nw,old:ℤ. ∀fmla:mFOL().
((¬(old ∈ mFOL-freevars(fmla)))
⇒ (mFOL-abstract(fmla[nw/old]) = mFOL-abstract(fmla) ∈ AbstractFOFormula(mFOL-freevars(fmla))))
Lemma: mFOL-subst-abstract
The evidence that fmla[x/y] in Dom, S, a is the same as the evidence
that fmla is true in Dom, S, a[y := a x].⋅
∀[Dom:Type]. ∀[S:FOStruct(Dom)]. ∀[fmla:mFOL()]. ∀[x,y:ℤ]. ∀[a:FOAssignment(mFOL-freevars(fmla[x/y]),Dom)].
(Dom,S,a |= mFOL-abstract(fmla[x/y]) = Dom,S,a[y := a x] |= mFOL-abstract(fmla) ∈ ℙ)
Definition: FOL-subst
fmla[nw/old] == mFOL-rename(FOL-rename-bound-to-avoid(fmla;[nw]);old;nw)
Lemma: FOL-subst_wf
∀[fmla:mFOL()]. ∀[nw,old:ℤ]. (fmla[nw/old] ∈ mFOL())
Lemma: freevars-FOL-subst
∀fmla:mFOL(). ∀nw,old,x:ℤ.
((x ∈ mFOL-freevars(fmla[nw/old]))
⇐⇒ ((¬(x = old ∈ ℤ)) ∧ (x ∈ mFOL-freevars(fmla))) ∨ ((x = nw ∈ ℤ) ∧ (old ∈ mFOL-freevars(fmla))))
Lemma: FOL-subst-abstract
The evidence that fmla[x/y] in Dom, S, a is the same as the evidence
that fmla is true in Dom, S, a[y := a x].⋅
∀[Dom:Type]. ∀[S:FOStruct+{i:l}(Dom)]. ∀[fmla:mFOL()]. ∀[x,y:ℤ]. ∀[a:FOAssignment(mFOL-freevars(fmla[x/y]),Dom)].
(Dom,S,a +|= FOL-abstract(fmla[x/y]) = Dom,S,a[y := a x] +|= FOL-abstract(fmla) ∈ ℙ)
Lemma: FOL-subst-trivial
∀nw,old:ℤ. ∀fmla:mFOL().
((¬(old ∈ mFOL-freevars(fmla)))
⇒ (FOL-abstract(fmla[nw/old]) = FOL-abstract(fmla) ∈ AbstractFOFormula+(mFOL-freevars(fmla))))
Definition: mFOL-evidence
mFOL-evidence(fmla) == mFO-uniform-evidence(mFOL-freevars(fmla);mFOL-abstract(fmla))
Lemma: mFOL-evidence_wf
∀[fmla:mFOL()]. (mFOL-evidence(fmla) ∈ 𝕌')
Lemma: mFOL-evidence-value-type
∀[fmla:mFOL()]. value-type(mFOL-evidence(fmla))
Definition: FOL-evidence
FOL-evidence{i:l}(fmla) == FO-uniform-evidence(mFOL-freevars(fmla);FOL-abstract(fmla))
Lemma: FOL-evidence_wf
∀[fmla:mFOL()]. (FOL-evidence{i:l}(fmla) ∈ 𝕌')
Definition: mFOLisImp
mFOLisImp(A) == mFOconnect?(A) ∧b mFOconnect-knd(A) =a "imp"
Lemma: mFOLisImp_wf
∀[A:mFOL()]. (mFOLisImp(A) ∈ 𝔹)
Definition: mFOLisAll
mFOLisAll(A) == mFOquant?(A) ∧b mFOquant-isall(A)
Lemma: mFOLisAll_wf
∀[A:mFOL()]. (mFOLisAll(A) ∈ 𝔹)
Definition: mFOLRule
mFOLRule() ==
lbl:Atom × if lbl =a "andI" then Unit
if lbl =a "impI" then Unit
if lbl =a "allI" then ℤ
if lbl =a "existsI" then ℤ
if lbl =a "orI" then 𝔹
if lbl =a "hyp" then Unit
if lbl =a "andE" then ℕ
if lbl =a "orE" then ℕ
if lbl =a "impE" then ℕ
if lbl =a "allE" then hypnum:ℕ × ℤ
if lbl =a "existsE" then hypnum:ℕ × ℤ
else Void
fi
Lemma: mFOLRule_wf
mFOLRule() ∈ Type
Lemma: mFOLRule-ext
mFOLRule() ≡ lbl:Atom × if lbl =a "andI" then Unit
if lbl =a "impI" then Unit
if lbl =a "allI" then ℤ
if lbl =a "existsI" then ℤ
if lbl =a "orI" then 𝔹
if lbl =a "hyp" then Unit
if lbl =a "andE" then ℕ
if lbl =a "orE" then ℕ
if lbl =a "impE" then ℕ
if lbl =a "allE" then hypnum:ℕ × ℤ
if lbl =a "existsE" then hypnum:ℕ × ℤ
else Void
fi
Definition: mRuleandI
andI == <"andI", ⋅>
Lemma: mRuleandI_wf
andI ∈ mFOLRule()
Definition: mRuleimpI
impI == <"impI", ⋅>
Lemma: mRuleimpI_wf
impI ∈ mFOLRule()
Definition: mRuleallI
allI with var == <"allI", var>
Lemma: mRuleallI_wf
∀[var:ℤ]. (allI with var ∈ mFOLRule())
Definition: mRuleexistsI
existsI with var == <"existsI", var>
Lemma: mRuleexistsI_wf
∀[var:ℤ]. (existsI with var ∈ mFOLRule())
Definition: mRuleorI
mRuleorI(left) == <"orI", left>
Lemma: mRuleorI_wf
∀[left:𝔹]. (mRuleorI(left) ∈ mFOLRule())
Definition: mRulehyp
hyp == <"hyp", ⋅>
Lemma: mRulehyp_wf
hyp ∈ mFOLRule()
Definition: mRuleandE
andE on hypnum == <"andE", hypnum>
Lemma: mRuleandE_wf
∀[hypnum:ℕ]. (andE on hypnum ∈ mFOLRule())
Definition: mRuleorE
orE on hypnum == <"orE", hypnum>
Lemma: mRuleorE_wf
∀[hypnum:ℕ]. (orE on hypnum ∈ mFOLRule())
Definition: mRuleimpE
impE on hypnum == <"impE", hypnum>
Lemma: mRuleimpE_wf
∀[hypnum:ℕ]. (impE on hypnum ∈ mFOLRule())
Definition: mRuleallE
allE on hypnum with var == <"allE", hypnum, var>
Lemma: mRuleallE_wf
∀[hypnum:ℕ]. ∀[var:ℤ]. (allE on hypnum with var ∈ mFOLRule())
Definition: mRuleexistsE
existsE on hypnum with var == <"existsE", hypnum, var>
Lemma: mRuleexistsE_wf
∀[hypnum:ℕ]. ∀[var:ℤ]. (existsE on hypnum with var ∈ mFOLRule())
Definition: mRuleandI?
mRuleandI?(v) == fst(v) =a "andI"
Lemma: mRuleandI?_wf
∀[v:mFOLRule()]. (mRuleandI?(v) ∈ 𝔹)
Definition: mRuleimpI?
mRuleimpI?(v) == fst(v) =a "impI"
Lemma: mRuleimpI?_wf
∀[v:mFOLRule()]. (mRuleimpI?(v) ∈ 𝔹)
Definition: mRuleallI?
mRuleallI?(v) == fst(v) =a "allI"
Lemma: mRuleallI?_wf
∀[v:mFOLRule()]. (mRuleallI?(v) ∈ 𝔹)
Definition: mRuleallI-var
mRuleallI-var(v) == snd(v)
Lemma: mRuleallI-var_wf
∀[v:mFOLRule()]. mRuleallI-var(v) ∈ ℤ supposing ↑mRuleallI?(v)
Definition: mRuleexistsI?
mRuleexistsI?(v) == fst(v) =a "existsI"
Lemma: mRuleexistsI?_wf
∀[v:mFOLRule()]. (mRuleexistsI?(v) ∈ 𝔹)
Definition: mRuleexistsI-var
mRuleexistsI-var(v) == snd(v)
Lemma: mRuleexistsI-var_wf
∀[v:mFOLRule()]. mRuleexistsI-var(v) ∈ ℤ supposing ↑mRuleexistsI?(v)
Definition: mRuleorI?
mRuleorI?(v) == fst(v) =a "orI"
Lemma: mRuleorI?_wf
∀[v:mFOLRule()]. (mRuleorI?(v) ∈ 𝔹)
Definition: mRuleorI-left
mRuleorI-left(v) == snd(v)
Lemma: mRuleorI-left_wf
∀[v:mFOLRule()]. mRuleorI-left(v) ∈ 𝔹 supposing ↑mRuleorI?(v)
Definition: mRulehyp?
mRulehyp?(v) == fst(v) =a "hyp"
Lemma: mRulehyp?_wf
∀[v:mFOLRule()]. (mRulehyp?(v) ∈ 𝔹)
Definition: mRuleandE?
mRuleandE?(v) == fst(v) =a "andE"
Lemma: mRuleandE?_wf
∀[v:mFOLRule()]. (mRuleandE?(v) ∈ 𝔹)
Definition: mRuleandE-hypnum
mRuleandE-hypnum(v) == snd(v)
Lemma: mRuleandE-hypnum_wf
∀[v:mFOLRule()]. mRuleandE-hypnum(v) ∈ ℕ supposing ↑mRuleandE?(v)
Definition: mRuleorE?
mRuleorE?(v) == fst(v) =a "orE"
Lemma: mRuleorE?_wf
∀[v:mFOLRule()]. (mRuleorE?(v) ∈ 𝔹)
Definition: mRuleorE-hypnum
mRuleorE-hypnum(v) == snd(v)
Lemma: mRuleorE-hypnum_wf
∀[v:mFOLRule()]. mRuleorE-hypnum(v) ∈ ℕ supposing ↑mRuleorE?(v)
Definition: mRuleimpE?
mRuleimpE?(v) == fst(v) =a "impE"
Lemma: mRuleimpE?_wf
∀[v:mFOLRule()]. (mRuleimpE?(v) ∈ 𝔹)
Definition: mRuleimpE-hypnum
mRuleimpE-hypnum(v) == snd(v)
Lemma: mRuleimpE-hypnum_wf
∀[v:mFOLRule()]. mRuleimpE-hypnum(v) ∈ ℕ supposing ↑mRuleimpE?(v)
Definition: mRuleallE?
mRuleallE?(v) == fst(v) =a "allE"
Lemma: mRuleallE?_wf
∀[v:mFOLRule()]. (mRuleallE?(v) ∈ 𝔹)
Definition: mRuleallE-hypnum
mRuleallE-hypnum(v) == fst(snd(v))
Lemma: mRuleallE-hypnum_wf
∀[v:mFOLRule()]. mRuleallE-hypnum(v) ∈ ℕ supposing ↑mRuleallE?(v)
Definition: mRuleallE-var
mRuleallE-var(v) == snd(snd(v))
Lemma: mRuleallE-var_wf
∀[v:mFOLRule()]. mRuleallE-var(v) ∈ ℤ supposing ↑mRuleallE?(v)
Definition: mRuleexistsE?
mRuleexistsE?(v) == fst(v) =a "existsE"
Lemma: mRuleexistsE?_wf
∀[v:mFOLRule()]. (mRuleexistsE?(v) ∈ 𝔹)
Definition: mRuleexistsE-hypnum
mRuleexistsE-hypnum(v) == fst(snd(v))
Lemma: mRuleexistsE-hypnum_wf
∀[v:mFOLRule()]. mRuleexistsE-hypnum(v) ∈ ℕ supposing ↑mRuleexistsE?(v)
Definition: mRuleexistsE-var
mRuleexistsE-var(v) == snd(snd(v))
Lemma: mRuleexistsE-var_wf
∀[v:mFOLRule()]. mRuleexistsE-var(v) ∈ ℤ supposing ↑mRuleexistsE?(v)
Lemma: mFOLRule-induction
∀[P:mFOLRule() ⟶ ℙ]
(P[andI]
⇒ P[impI]
⇒ (∀var:ℤ. P[allI with var])
⇒ (∀var:ℤ. P[existsI with var])
⇒ (∀left:𝔹. P[mRuleorI(left)])
⇒ P[hyp]
⇒ (∀hypnum:ℕ. P[andE on hypnum])
⇒ (∀hypnum:ℕ. P[orE on hypnum])
⇒ (∀hypnum:ℕ. P[impE on hypnum])
⇒ (∀hypnum:ℕ. ∀var:ℤ. P[allE on hypnum with var])
⇒ (∀hypnum:ℕ. ∀var:ℤ. P[existsE on hypnum with var])
⇒ {∀v:mFOLRule(). P[v]})
Lemma: mFOLRule-definition
∀[A:Type]. ∀[R:A ⟶ mFOLRule() ⟶ ℙ].
({x:A| R[x;andI]}
⇒ {x:A| R[x;impI]}
⇒ (∀var:ℤ. {x:A| R[x;allI with var]} )
⇒ (∀var:ℤ. {x:A| R[x;existsI with var]} )
⇒ (∀left:𝔹. {x:A| R[x;mRuleorI(left)]} )
⇒ {x:A| R[x;hyp]}
⇒ (∀hypnum:ℕ. {x:A| R[x;andE on hypnum]} )
⇒ (∀hypnum:ℕ. {x:A| R[x;orE on hypnum]} )
⇒ (∀hypnum:ℕ. {x:A| R[x;impE on hypnum]} )
⇒ (∀hypnum:ℕ. ∀var:ℤ. {x:A| R[x;allE on hypnum with var]} )
⇒ (∀hypnum:ℕ. ∀var:ℤ. {x:A| R[x;existsE on hypnum with var]} )
⇒ {∀v:mFOLRule(). {x:A| R[x;v]} })
Definition: mFOLRule_ind
case(v)
andI => andI
impI => impI
allI with var => allI[var]
existsI with var => existsI[var]
orI (left?left) => orI[left]
hyp => hyp
andE @hypnum => andE[hypnum]
orE @hypnum => orE[hypnum]
impE @hypnum => impE[hypnum]
allE @hypnum with var => allE[hypnum; var]
existsE @hypnum with var => existsE[hypnum; var] ==
let lbl,v1 = v
in if lbl="andI" then andI
if lbl="impI" then impI
if lbl="allI" then allI[v1]
if lbl="existsI" then existsI[v1]
if lbl="orI" then orI[v1]
if lbl="hyp" then hyp
if lbl="andE" then andE[v1]
if lbl="orE" then orE[v1]
if lbl="impE" then impE[v1]
if lbl="allE" then let hypnum,v2 = v1 in allE[hypnum; v2]
if lbl="existsE" then let hypnum,v2 = v1 in existsE[hypnum; v2]
else Ax
fi
Lemma: mFOLRule_ind_wf
∀[A:Type]. ∀[R:A ⟶ mFOLRule() ⟶ ℙ]. ∀[v:mFOLRule()]. ∀[andI:{x:A| R[x;andI]} ]. ∀[impI:{x:A| R[x;impI]} ].
∀[allI:var:ℤ ⟶ {x:A| R[x;allI with var]} ]. ∀[existsI:var:ℤ ⟶ {x:A| R[x;existsI with var]} ].
∀[orI:left:𝔹 ⟶ {x:A| R[x;mRuleorI(left)]} ]. ∀[hyp:{x:A| R[x;hyp]} ]. ∀[andE:hypnum:ℕ ⟶ {x:A| R[x;andE on hypnum]} ].
∀[orE:hypnum:ℕ ⟶ {x:A| R[x;orE on hypnum]} ]. ∀[impE:hypnum:ℕ ⟶ {x:A| R[x;impE on hypnum]} ].
∀[allE:hypnum:ℕ ⟶ var:ℤ ⟶ {x:A| R[x;allE on hypnum with var]} ]. ∀[existsE:hypnum:ℕ
⟶ var:ℤ
⟶ {x:A| R[x;existsE on hypnum with var]} ].
(case(v)
andI => andI
impI => impI
allI with var => allI[var]
existsI with var => existsI[var]
orI (left?left) => orI[left]
hyp => hyp
andE @hypnum => andE[hypnum]
orE @hypnum => orE[hypnum]
impE @hypnum => impE[hypnum]
allE @hypnum with var => allE[hypnum;var]
existsE @hypnum with var => existsE[hypnum;var] ∈ {x:A| R[x;v]} )
Lemma: mFOLRule_ind_wf_simple
∀[A:Type]. ∀[v:mFOLRule()]. ∀[andI,impI:A]. ∀[allI,existsI:var:ℤ ⟶ A]. ∀[orI:left:𝔹 ⟶ A]. ∀[hyp:A].
∀[andE,orE,impE:hypnum:ℕ ⟶ A]. ∀[allE,existsE:hypnum:ℕ ⟶ var:ℤ ⟶ A].
(case(v)
andI => andI
impI => impI
allI with var => allI[var]
existsI with var => existsI[var]
orI (left?left) => orI[left]
hyp => hyp
andE @hypnum => andE[hypnum]
orE @hypnum => orE[hypnum]
impE @hypnum => impE[hypnum]
allE @hypnum with var => allE[hypnum;var]
existsE @hypnum with var => existsE[hypnum;var] ∈ A)
Definition: FOLRule
FOLRule() ==
lbl:Atom × if lbl =a "andI" then Unit
if lbl =a "impI" then Unit
if lbl =a "allI" then ℤ
if lbl =a "existsI" then ℤ
if lbl =a "orI" then 𝔹
if lbl =a "hyp" then Unit
if lbl =a "andE" then ℕ
if lbl =a "orE" then ℕ
if lbl =a "impE" then ℕ
if lbl =a "allE" then hypnum:ℕ × ℤ
if lbl =a "existsE" then hypnum:ℕ × ℤ
if lbl =a "falseE" then ℕ
else Void
fi
Lemma: FOLRule_wf
FOLRule() ∈ Type
Lemma: FOLRule-ext
FOLRule() ≡ lbl:Atom × if lbl =a "andI" then Unit
if lbl =a "impI" then Unit
if lbl =a "allI" then ℤ
if lbl =a "existsI" then ℤ
if lbl =a "orI" then 𝔹
if lbl =a "hyp" then Unit
if lbl =a "andE" then ℕ
if lbl =a "orE" then ℕ
if lbl =a "impE" then ℕ
if lbl =a "allE" then hypnum:ℕ × ℤ
if lbl =a "existsE" then hypnum:ℕ × ℤ
if lbl =a "falseE" then ℕ
else Void
fi
Definition: fRuleandI
andI == <"andI", ⋅>
Lemma: fRuleandI_wf
andI ∈ FOLRule()
Definition: fRuleimpI
impI == <"impI", ⋅>
Lemma: fRuleimpI_wf
impI ∈ FOLRule()
Definition: fRuleallI
allI with var == <"allI", var>
Lemma: fRuleallI_wf
∀[var:ℤ]. (allI with var ∈ FOLRule())
Definition: fRuleexistsI
existsI with var == <"existsI", var>
Lemma: fRuleexistsI_wf
∀[var:ℤ]. (existsI with var ∈ FOLRule())
Definition: fRuleorI
fRuleorI(left) == <"orI", left>
Lemma: fRuleorI_wf
∀[left:𝔹]. (fRuleorI(left) ∈ FOLRule())
Definition: fRulehyp
hyp == <"hyp", ⋅>
Lemma: fRulehyp_wf
hyp ∈ FOLRule()
Definition: fRuleandE
andE on hypnum == <"andE", hypnum>
Lemma: fRuleandE_wf
∀[hypnum:ℕ]. (andE on hypnum ∈ FOLRule())
Definition: fRuleorE
orE on hypnum == <"orE", hypnum>
Lemma: fRuleorE_wf
∀[hypnum:ℕ]. (orE on hypnum ∈ FOLRule())
Definition: fRuleimpE
impE on hypnum == <"impE", hypnum>
Lemma: fRuleimpE_wf
∀[hypnum:ℕ]. (impE on hypnum ∈ FOLRule())
Definition: fRuleallE
allE on hypnum with var == <"allE", hypnum, var>
Lemma: fRuleallE_wf
∀[hypnum:ℕ]. ∀[var:ℤ]. (allE on hypnum with var ∈ FOLRule())
Definition: fRuleexistsE
existsE on hypnum with var == <"existsE", hypnum, var>
Lemma: fRuleexistsE_wf
∀[hypnum:ℕ]. ∀[var:ℤ]. (existsE on hypnum with var ∈ FOLRule())
Definition: fRulefalseE
falseE on hypnum == <"falseE", hypnum>
Lemma: fRulefalseE_wf
∀[hypnum:ℕ]. (falseE on hypnum ∈ FOLRule())
Definition: fRuleandI?
fRuleandI?(v) == fst(v) =a "andI"
Lemma: fRuleandI?_wf
∀[v:FOLRule()]. (fRuleandI?(v) ∈ 𝔹)
Definition: fRuleimpI?
fRuleimpI?(v) == fst(v) =a "impI"
Lemma: fRuleimpI?_wf
∀[v:FOLRule()]. (fRuleimpI?(v) ∈ 𝔹)
Definition: fRuleallI?
fRuleallI?(v) == fst(v) =a "allI"
Lemma: fRuleallI?_wf
∀[v:FOLRule()]. (fRuleallI?(v) ∈ 𝔹)
Definition: fRuleallI-var
fRuleallI-var(v) == snd(v)
Lemma: fRuleallI-var_wf
∀[v:FOLRule()]. fRuleallI-var(v) ∈ ℤ supposing ↑fRuleallI?(v)
Definition: fRuleexistsI?
fRuleexistsI?(v) == fst(v) =a "existsI"
Lemma: fRuleexistsI?_wf
∀[v:FOLRule()]. (fRuleexistsI?(v) ∈ 𝔹)
Definition: fRuleexistsI-var
fRuleexistsI-var(v) == snd(v)
Lemma: fRuleexistsI-var_wf
∀[v:FOLRule()]. fRuleexistsI-var(v) ∈ ℤ supposing ↑fRuleexistsI?(v)
Definition: fRuleorI?
fRuleorI?(v) == fst(v) =a "orI"
Lemma: fRuleorI?_wf
∀[v:FOLRule()]. (fRuleorI?(v) ∈ 𝔹)
Definition: fRuleorI-left
fRuleorI-left(v) == snd(v)
Lemma: fRuleorI-left_wf
∀[v:FOLRule()]. fRuleorI-left(v) ∈ 𝔹 supposing ↑fRuleorI?(v)
Definition: fRulehyp?
fRulehyp?(v) == fst(v) =a "hyp"
Lemma: fRulehyp?_wf
∀[v:FOLRule()]. (fRulehyp?(v) ∈ 𝔹)
Definition: fRuleandE?
fRuleandE?(v) == fst(v) =a "andE"
Lemma: fRuleandE?_wf
∀[v:FOLRule()]. (fRuleandE?(v) ∈ 𝔹)
Definition: fRuleandE-hypnum
fRuleandE-hypnum(v) == snd(v)
Lemma: fRuleandE-hypnum_wf
∀[v:FOLRule()]. fRuleandE-hypnum(v) ∈ ℕ supposing ↑fRuleandE?(v)
Definition: fRuleorE?
fRuleorE?(v) == fst(v) =a "orE"
Lemma: fRuleorE?_wf
∀[v:FOLRule()]. (fRuleorE?(v) ∈ 𝔹)
Definition: fRuleorE-hypnum
fRuleorE-hypnum(v) == snd(v)
Lemma: fRuleorE-hypnum_wf
∀[v:FOLRule()]. fRuleorE-hypnum(v) ∈ ℕ supposing ↑fRuleorE?(v)
Definition: fRuleimpE?
fRuleimpE?(v) == fst(v) =a "impE"
Lemma: fRuleimpE?_wf
∀[v:FOLRule()]. (fRuleimpE?(v) ∈ 𝔹)
Definition: fRuleimpE-hypnum
fRuleimpE-hypnum(v) == snd(v)
Lemma: fRuleimpE-hypnum_wf
∀[v:FOLRule()]. fRuleimpE-hypnum(v) ∈ ℕ supposing ↑fRuleimpE?(v)
Definition: fRuleallE?
fRuleallE?(v) == fst(v) =a "allE"
Lemma: fRuleallE?_wf
∀[v:FOLRule()]. (fRuleallE?(v) ∈ 𝔹)
Definition: fRuleallE-hypnum
fRuleallE-hypnum(v) == fst(snd(v))
Lemma: fRuleallE-hypnum_wf
∀[v:FOLRule()]. fRuleallE-hypnum(v) ∈ ℕ supposing ↑fRuleallE?(v)
Definition: fRuleallE-var
fRuleallE-var(v) == snd(snd(v))
Lemma: fRuleallE-var_wf
∀[v:FOLRule()]. fRuleallE-var(v) ∈ ℤ supposing ↑fRuleallE?(v)
Definition: fRuleexistsE?
fRuleexistsE?(v) == fst(v) =a "existsE"
Lemma: fRuleexistsE?_wf
∀[v:FOLRule()]. (fRuleexistsE?(v) ∈ 𝔹)
Definition: fRuleexistsE-hypnum
fRuleexistsE-hypnum(v) == fst(snd(v))
Lemma: fRuleexistsE-hypnum_wf
∀[v:FOLRule()]. fRuleexistsE-hypnum(v) ∈ ℕ supposing ↑fRuleexistsE?(v)
Definition: fRuleexistsE-var
fRuleexistsE-var(v) == snd(snd(v))
Lemma: fRuleexistsE-var_wf
∀[v:FOLRule()]. fRuleexistsE-var(v) ∈ ℤ supposing ↑fRuleexistsE?(v)
Definition: fRulefalseE?
fRulefalseE?(v) == fst(v) =a "falseE"
Lemma: fRulefalseE?_wf
∀[v:FOLRule()]. (fRulefalseE?(v) ∈ 𝔹)
Definition: fRulefalseE-hypnum
fRulefalseE-hypnum(v) == snd(v)
Lemma: fRulefalseE-hypnum_wf
∀[v:FOLRule()]. fRulefalseE-hypnum(v) ∈ ℕ supposing ↑fRulefalseE?(v)
Lemma: FOLRule-induction
∀[P:FOLRule() ⟶ ℙ]
(P[andI]
⇒ P[impI]
⇒ (∀var:ℤ. P[allI with var])
⇒ (∀var:ℤ. P[existsI with var])
⇒ (∀left:𝔹. P[fRuleorI(left)])
⇒ P[hyp]
⇒ (∀hypnum:ℕ. P[andE on hypnum])
⇒ (∀hypnum:ℕ. P[orE on hypnum])
⇒ (∀hypnum:ℕ. P[impE on hypnum])
⇒ (∀hypnum:ℕ. ∀var:ℤ. P[allE on hypnum with var])
⇒ (∀hypnum:ℕ. ∀var:ℤ. P[existsE on hypnum with var])
⇒ (∀hypnum:ℕ. P[falseE on hypnum])
⇒ {∀v:FOLRule(). P[v]})
Lemma: FOLRule-definition
∀[A:Type]. ∀[R:A ⟶ FOLRule() ⟶ ℙ].
({x:A| R[x;andI]}
⇒ {x:A| R[x;impI]}
⇒ (∀var:ℤ. {x:A| R[x;allI with var]} )
⇒ (∀var:ℤ. {x:A| R[x;existsI with var]} )
⇒ (∀left:𝔹. {x:A| R[x;fRuleorI(left)]} )
⇒ {x:A| R[x;hyp]}
⇒ (∀hypnum:ℕ. {x:A| R[x;andE on hypnum]} )
⇒ (∀hypnum:ℕ. {x:A| R[x;orE on hypnum]} )
⇒ (∀hypnum:ℕ. {x:A| R[x;impE on hypnum]} )
⇒ (∀hypnum:ℕ. ∀var:ℤ. {x:A| R[x;allE on hypnum with var]} )
⇒ (∀hypnum:ℕ. ∀var:ℤ. {x:A| R[x;existsE on hypnum with var]} )
⇒ (∀hypnum:ℕ. {x:A| R[x;falseE on hypnum]} )
⇒ {∀v:FOLRule(). {x:A| R[x;v]} })
Definition: FOLRule_ind
case(v)
andI => andI
impI => impI
allI with var => allI[var]
existsI with var => existsI[var]
orI (left?left) => orI[left]
hyp => hyp
andE @hypnum => andE[hypnum]
orE @hypnum => orE[hypnum]
impE @hypnum => impE[hypnum]
allE @hypnum with var => allE[hypnum; var]
existsE @hypnum with var => existsE[hypnum; var]
falseE @hypnum => falseE[hypnum] ==
let lbl,v1 = v
in if lbl="andI" then andI
if lbl="impI" then impI
if lbl="allI" then allI[v1]
if lbl="existsI" then existsI[v1]
if lbl="orI" then orI[v1]
if lbl="hyp" then hyp
if lbl="andE" then andE[v1]
if lbl="orE" then orE[v1]
if lbl="impE" then impE[v1]
if lbl="allE" then let hypnum,v2 = v1 in allE[hypnum; v2]
if lbl="existsE" then let hypnum,v2 = v1 in existsE[hypnum; v2]
if lbl="falseE" then falseE[v1]
else Ax
fi
Lemma: FOLRule_ind_wf
∀[A:Type]. ∀[R:A ⟶ FOLRule() ⟶ ℙ]. ∀[v:FOLRule()]. ∀[andI:{x:A| R[x;andI]} ]. ∀[impI:{x:A| R[x;impI]} ].
∀[allI:var:ℤ ⟶ {x:A| R[x;allI with var]} ]. ∀[existsI:var:ℤ ⟶ {x:A| R[x;existsI with var]} ].
∀[orI:left:𝔹 ⟶ {x:A| R[x;fRuleorI(left)]} ]. ∀[hyp:{x:A| R[x;hyp]} ]. ∀[andE:hypnum:ℕ ⟶ {x:A| R[x;andE on hypnum]} ].
∀[orE:hypnum:ℕ ⟶ {x:A| R[x;orE on hypnum]} ]. ∀[impE:hypnum:ℕ ⟶ {x:A| R[x;impE on hypnum]} ].
∀[allE:hypnum:ℕ ⟶ var:ℤ ⟶ {x:A| R[x;allE on hypnum with var]} ]. ∀[existsE:hypnum:ℕ
⟶ var:ℤ
⟶ {x:A| R[x;existsE on hypnum with var]} ].
∀[falseE:hypnum:ℕ ⟶ {x:A| R[x;falseE on hypnum]} ].
(case(v)
andI => andI
impI => impI
allI with var => allI[var]
existsI with var => existsI[var]
orI (left?left) => orI[left]
hyp => hyp
andE @hypnum => andE[hypnum]
orE @hypnum => orE[hypnum]
impE @hypnum => impE[hypnum]
allE @hypnum with var => allE[hypnum;var]
existsE @hypnum with var => existsE[hypnum;var]
falseE @hypnum => falseE[hypnum] ∈ {x:A| R[x;v]} )
Lemma: FOLRule_ind_wf_simple
∀[A:Type]. ∀[v:FOLRule()]. ∀[andI,impI:A]. ∀[allI,existsI:var:ℤ ⟶ A]. ∀[orI:left:𝔹 ⟶ A]. ∀[hyp:A].
∀[andE,orE,impE:hypnum:ℕ ⟶ A]. ∀[allE,existsE:hypnum:ℕ ⟶ var:ℤ ⟶ A]. ∀[falseE:hypnum:ℕ ⟶ A].
(case(v)
andI => andI
impI => impI
allI with var => allI[var]
existsI with var => existsI[var]
orI (left?left) => orI[left]
hyp => hyp
andE @hypnum => andE[hypnum]
orE @hypnum => orE[hypnum]
impE @hypnum => impE[hypnum]
allE @hypnum with var => allE[hypnum;var]
existsE @hypnum with var => existsE[hypnum;var]
falseE @hypnum => falseE[hypnum] ∈ A)
Lemma: FOLRule-induction-ext
∀[P:FOLRule() ⟶ ℙ]
(P[andI]
⇒ P[impI]
⇒ (∀var:ℤ. P[allI with var])
⇒ (∀var:ℤ. P[existsI with var])
⇒ (∀left:𝔹. P[fRuleorI(left)])
⇒ P[hyp]
⇒ (∀hypnum:ℕ. P[andE on hypnum])
⇒ (∀hypnum:ℕ. P[orE on hypnum])
⇒ (∀hypnum:ℕ. P[impE on hypnum])
⇒ (∀hypnum:ℕ. ∀var:ℤ. P[allE on hypnum with var])
⇒ (∀hypnum:ℕ. ∀var:ℤ. P[existsE on hypnum with var])
⇒ (∀hypnum:ℕ. P[falseE on hypnum])
⇒ {∀v:FOLRule(). P[v]})
Definition: mFOL-sequent
A sequent for mFOL is a list of hypothesis and a conclusion.⋅
mFOL-sequent() == mFOL() List × mFOL()
Lemma: mFOL-sequent_wf
mFOL-sequent() ∈ Type
Definition: mk_mFOLSequent
hyps ⊢ concl == <hyps, concl>
Lemma: mk_mFOLSequent_wf
∀[hyps:mFOL() List]. ∀[concl:mFOL()]. (hyps ⊢ concl ∈ mFOL-sequent())
Definition: mFOL-sequent-freevars
mFOL-sequent-freevars(s) == let hs,c = s in reduce(λh,vs. mFOL-freevars(h) ⋃ vs;mFOL-freevars(c);hs)
Lemma: mFOL-sequent-freevars_wf
∀[s:mFOL-sequent()]. (mFOL-sequent-freevars(s) ∈ ℤ List)
Lemma: mFOL-sequent-freevars-contained
∀s:mFOL-sequent(). ∀L:ℤ List.
(mFOL-sequent-freevars(s) ⊆ L ⇐⇒ mFOL-freevars(snd(s)) ⊆ L ∧ (∀h:mFOL(). ((h ∈ fst(s)) ⇒ mFOL-freevars(h) ⊆ L)))
Lemma: not-member-mFOL-sequent-freevars
∀s:mFOL-sequent(). ∀v:ℤ.
(¬(v ∈ mFOL-sequent-freevars(s)) ⇐⇒ (¬(v ∈ mFOL-freevars(snd(s)))) ∧ (∀h∈fst(s).¬(v ∈ mFOL-freevars(h))))
Lemma: member-mFOL-sequent-freevars
∀s:mFOL-sequent(). ∀v:ℤ.
((v ∈ mFOL-sequent-freevars(s)) ⇐⇒ (v ∈ mFOL-freevars(snd(s))) ∨ (∃h∈fst(s). (v ∈ mFOL-freevars(h))))
Lemma: mFOL-sequent-freevars-contains-concl
∀s:mFOL-sequent(). ∀L:ℤ List. (L ⊆ mFOL-freevars(snd(s)) ⇒ L ⊆ mFOL-sequent-freevars(s))
Lemma: mFOL-sequent-freevars-subset-1
∀hyps:mFOL() List. ∀concl:mFOL(). mFOL-freevars(concl) ⊆ mFOL-sequent-freevars(<hyps, concl>)
Lemma: mFOL-sequent-freevars-subset-2
∀hyps:mFOL() List. ∀concl,h:mFOL(). ((h ∈ hyps) ⇒ mFOL-freevars(h) ⊆ mFOL-sequent-freevars(<hyps, concl>))
Lemma: mFOL-sequent-freevars-subset-4
∀hyps:mFOL() List. ∀x,y:mFOL(). (mFOL-freevars(x) ⊆ mFOL-sequent-freevars(<hyps, y>) ⇒ mFOL-sequent-freevars(<hyps, x>\000C) ⊆ mFOL-sequent-freevars(<hyps, y>))
Lemma: mFOL-sequent-freevars-subset-3
∀hyps:mFOL() List. ∀x,y:mFOL(). (mFOL-freevars(x) ⊆ mFOL-freevars(y) ⇒ mFOL-sequent-freevars(<hyps, x>) ⊆ mFOL-sequent\000C-freevars(<hyps, y>))
Definition: mFOL-hyps-meaning
mFOL-hyps-meaning(Dom;S;a;hyps) == map(λh.Dom,S,a |= mFOL-abstract(h);hyps)
Lemma: mFOL-hyps-meaning_wf
∀[concl:mFOL()]. ∀[hyps:mFOL() List]. ∀[Dom:Type]. ∀[S:FOStruct(Dom)]. ∀[a:FOAssignment(mFOL-sequent-freevars(<hyps
, concl
>),Dom)].
(mFOL-hyps-meaning(Dom;S;a;hyps) ∈ Type List)
Lemma: mFOL-hyps-meaning-cons
∀[hyps,Dom,S,a,x:Top].
(tuple-type(mFOL-hyps-meaning(Dom;S;a;[x / hyps])) ~ if null(hyps)
then Dom,S,a |= mFOL-abstract(x)
else Dom,S,a |= mFOL-abstract(x) × tuple-type(mFOL-hyps-meaning(Dom;S;a;hyps))
fi )
Definition: FOL-hyps-meaning
FOL-hyps-meaning(Dom;S;a;hyps) == map(λh.Dom,S,a +|= FOL-abstract(h);hyps)
Lemma: FOL-hyps-meaning_wf
∀[concl:mFOL()]. ∀[hyps:mFOL() List]. ∀[Dom:Type]. ∀[S:FOStruct+{i:l}(Dom)].
∀[a:FOAssignment(mFOL-sequent-freevars(<hyps, concl>),Dom)].
(FOL-hyps-meaning(Dom;S;a;hyps) ∈ Type List)
Lemma: FOL-hyps-meaning-cons
∀[hyps,Dom,S,a,x:Top].
(tuple-type(FOL-hyps-meaning(Dom;S;a;[x / hyps])) ~ if null(hyps)
then Dom,S,a +|= FOL-abstract(x)
else Dom,S,a +|= FOL-abstract(x) × tuple-type(FOL-hyps-meaning(Dom;S;a;hyps))
fi )
Definition: mFOL-sequent-abstract
The abstract meaning of a sequent is a function
from the tuple of abstract meanings of the hypotheses to
the abstract meaning of the conclusion.⋅
mFOL-sequent-abstract(s) ==
let hyps,concl = s
in λDom,S,a. (tuple-type(mFOL-hyps-meaning(Dom;S;a;hyps)) ⟶ Dom,S,a |= mFOL-abstract(concl))
Lemma: mFOL-sequent-abstract_wf
∀[s:mFOL-sequent()]. (mFOL-sequent-abstract(s) ∈ AbstractFOFormula(mFOL-sequent-freevars(s)))
Definition: FOL-sequent-abstract
FOL-sequent-abstract(s) ==
let hyps,concl = s
in λDom,S,a. (tuple-type(FOL-hyps-meaning(Dom;S;a;hyps)) ⟶ Dom,S,a +|= FOL-abstract(concl))
Lemma: FOL-sequent-abstract_wf
∀[s:mFOL-sequent()]. (FOL-sequent-abstract(s) ∈ AbstractFOFormula+(mFOL-sequent-freevars(s)))
Definition: mFOL-sequent-evidence
mFOL-sequent-evidence(s) == mFO-uniform-evidence(mFOL-sequent-freevars(s);mFOL-sequent-abstract(s))
Lemma: mFOL-sequent-evidence_wf
∀[s:mFOL-sequent()]. (mFOL-sequent-evidence(s) ∈ 𝕌')
Definition: FOL-sequent-evidence
FOL-sequent-evidence{i:l}(s) == FO-uniform-evidence(mFOL-sequent-freevars(s);FOL-sequent-abstract(s))
Lemma: FOL-sequent-evidence_wf
∀[s:mFOL-sequent()]. (FOL-sequent-evidence{i:l}(s) ∈ 𝕌')
Lemma: mFOL-sequent-evidence-trivial
Uniform evidence for a trivially true sequent where the conclusion is
a given member of the hypotheses.⋅
∀hyps:mFOL() List. ∀i:ℕ||hyps||. mFOL-sequent-evidence(<hyps, hyps[i]>)
Lemma: FOL-sequent-evidence-trivial
Uniform evidence for a trivially true sequent where the conclusion is
a given member of the hypotheses.⋅
∀hyps:mFOL() List. ∀i:ℕ||hyps||. FOL-sequent-evidence{i:l}(<hyps, hyps[i]>)
Lemma: mFOL-sequent-evidence_transitivity1
From uniform evidence that hyps ⇒ x and uniform evidence that x ⇒ y
we construct uniform evidence that hyps ⇒ y.⋅
∀[hyps:mFOL() List]. ∀[x,y:mFOL()].
(mFOL-freevars(x) ⊆ mFOL-freevars(y)
⇒ (∀[Dom:Type]. ∀[S:FOStruct(Dom)].
∀a:FOAssignment(mFOL-freevars(y),Dom). (Dom,S,a |= mFOL-abstract(x) ⇒ Dom,S,a |= mFOL-abstract(y)))
⇒ mFOL-sequent-evidence(<hyps, x>)
⇒ mFOL-sequent-evidence(<hyps, y>))
Lemma: better-mFOL-sequent-evidence_transitivity1
From uniform evidence that hyps ⇒ x and uniform evidence that x ⇒ y
we construct uniform evidence that hyps ⇒ y.⋅
∀[hyps:mFOL() List]. ∀[x,y:mFOL()].
(mFOL-freevars(x) ⊆ mFOL-sequent-freevars(<hyps, y>)
⇒ (∀[Dom:Type]. ∀[S:FOStruct(Dom)].
∀a:FOAssignment(mFOL-sequent-freevars(<hyps, y>),Dom). (Dom,S,a |= mFOL-abstract(x) ⇒ Dom,S,a |= mFOL-abstract(\000Cy)))
⇒ mFOL-sequent-evidence(<hyps, x>)
⇒ mFOL-sequent-evidence(<hyps, y>))
Lemma: FOL-sequent-evidence_transitivity1
From uniform evidence that hyps ⇒ x and uniform evidence that x ⇒ y
we construct uniform evidence that hyps ⇒ y.⋅
∀[hyps:mFOL() List]. ∀[x,y:mFOL()].
(mFOL-freevars(x) ⊆ mFOL-freevars(y)
⇒ (∀[Dom:Type]. ∀[S:FOStruct+{i:l}(Dom)].
∀a:FOAssignment(mFOL-freevars(y),Dom). (Dom,S,a +|= FOL-abstract(x) ⇒ Dom,S,a +|= FOL-abstract(y)))
⇒ FOL-sequent-evidence{i:l}(<hyps, x>)
⇒ FOL-sequent-evidence{i:l}(<hyps, y>))
Lemma: better-FOL-sequent-evidence_transitivity1
From uniform evidence that hyps ⇒ x and uniform evidence that x ⇒ y
we construct uniform evidence that hyps ⇒ y.⋅
∀[hyps:mFOL() List]. ∀[x,y:mFOL()].
(mFOL-freevars(x) ⊆ mFOL-sequent-freevars(<hyps, y>)
⇒ (∀[Dom:Type]. ∀[S:FOStruct+{i:l}(Dom)].
∀a:FOAssignment(mFOL-sequent-freevars(<hyps, y>),Dom). (Dom,S,a +|= FOL-abstract(x) ⇒ Dom,S,a +|= FOL-abstract(\000Cy)))
⇒ FOL-sequent-evidence{i:l}(<hyps, x>)
⇒ FOL-sequent-evidence{i:l}(<hyps, y>))
Lemma: mFOL-sequent-evidence_transitivity2
From uniform evidence that hyps ⇒ y and
uniform evidence that (y ∧ hyps) ⇒ x
we construct uniform evidence that hyps ⇒ x.⋅
∀hyps:mFOL() List. ∀[x,y:mFOL()]. (mFOL-freevars(y) ⊆ mFOL-sequent-freevars(<hyps, x>) ⇒ mFOL-sequent-evidence(<hyps, \000Cy>) ⇒ mFOL-sequent-evidence(<[y / hyps], x>) ⇒ mFOL-sequent-evidence(<hyps, x>))
Lemma: FOL-sequent-evidence_transitivity2
From uniform evidence that hyps ⇒ y and
uniform evidence that (y ∧ hyps) ⇒ x
we construct uniform evidence that hyps ⇒ x.⋅
∀hyps:mFOL() List. ∀[x,y:mFOL()]. (mFOL-freevars(y) ⊆ mFOL-sequent-freevars(<hyps, x>) ⇒ FOL-sequent-evidence{i:l}(<hy\000Cps, y>) ⇒ FOL-sequent-evidence{i:l}(<[y / hyps], x>) ⇒ FOL-sequent-evidence{i:l}(<hyps, x>))
Lemma: mFOL-sequent-evidence_and
From uniform evidence that hyps ⇒ x and
uniform evidence that (y ∧ hyps) ⇒ y
we construct uniform evidence that hyps ⇒ x ∧ y⋅
∀hyps:mFOL() List. ∀[x,y:mFOL()]. (mFOL-sequent-evidence(<hyps, x>) ⇒ mFOL-sequent-evidence(<hyps, y>) ⇒ mFOL-sequent\000C-evidence(<hyps, x ∧ y>))
Lemma: FOL-sequent-evidence_and
From uniform evidence that hyps ⇒ x and
uniform evidence that (y ∧ hyps) ⇒ y
we construct uniform evidence that hyps ⇒ x ∧ y⋅
∀hyps:mFOL() List. ∀[x,y:mFOL()]. (FOL-sequent-evidence{i:l}(<hyps, x>) ⇒ FOL-sequent-evidence{i:l}(<hyps, y>) ⇒ FOL-\000Csequent-evidence{i:l}(<hyps, x ∧ y>))
Definition: mFOLeffect
The effect of a given rule r on a given mFOL sequent s.
If the rule does not apply, then it `fails` by producing the effect ⌜inr ⋅ ⌝
otherwise it succeeds and produces ⌜inl L⌝where L is the list of subgoal sequents.⋅
mFOLeffect(sr) ==
let s,r = sr
in let hyps,concl = s
in case(r)
andI => let a,b = dest-"and"(concl) in
inl [<hyps, a>; <hyps, b>]
impI => let a,b = dest-"imp"(concl) in
inl [<[a / hyps], b>]
allI with v => if ¬bv ∈b mFOL-sequent-freevars(<hyps, concl>) then let x,b = dest-all(concl); in inl [<hyps, b[v\000C/x]>] else inr ⋅ fi
existsI with v => if v ∈b mFOL-sequent-freevars(<hyps, concl>) then let x,b = dest-exists(concl); in inl [<hyps,\000C b[v/x]>] else inr ⋅ fi
orI (left?x) => let a,b = dest-"or"(concl) in
inl [<hyps, if x then a else b fi >]
hyp => if concl ∈b hyps then inl [] else inr ⋅ fi
andE @i => if i <z ||hyps|| then let a,b = dest-"and"(hyps[i]) in inl [<[a; [b / hyps]], concl>] else inr ⋅ fi
orE @i => if i <z ||hyps|| then let a,b = dest-"or"(hyps[i]) in inl [<[a / hyps], concl>; <[b / hyps], concl>] e\000Clse inr ⋅ fi
impE @i => if i <z ||hyps|| then let a,b = dest-"imp"(hyps[i]) in inl [<hyps, a>; <[b / hyps], concl>] else inr \000C⋅ fi
allE @i with v => if i <z ||hyps|| ∧b v ∈b mFOL-sequent-freevars(<hyps, concl>)
then let x,b = dest-all(hyps[i]); in
inl [<[b[v/x] / hyps], concl>]
else inr ⋅
fi
existsE @i with v => if i <z ||hyps|| ∧b (¬bv ∈b mFOL-sequent-freevars(<hyps, concl>))
then let x,b = dest-exists(hyps[i]); in
inl [<[b[v/x] / hyps], concl>]
else inr ⋅
fi
falseE @i => inr ⋅
Lemma: mFOLeffect_wf
∀[sr:mFOL-sequent() × FOLRule()]. (mFOLeffect(sr) ∈ mFOL-sequent() List?)
Definition: FOLeffect
FOLeffect(sr) ==
let s,r = sr
in let hyps,concl = s
in case(r)
andI => let a,b = dest-"and"(concl) in
inl [<hyps, a>; <hyps, b>]
impI => let a,b = dest-"imp"(concl) in
inl [<[a / hyps], b>]
allI with v => if ¬bv ∈b mFOL-sequent-freevars(<hyps, concl>) then let x,b = dest-all(concl); in inl [<hyps, b[v\000C/x]>] else inr ⋅ fi
existsI with v => if v ∈b mFOL-sequent-freevars(<hyps, concl>) then let x,b = dest-exists(concl); in inl [<hyps,\000C b[v/x]>] else inr ⋅ fi
orI (left?x) => let a,b = dest-"or"(concl) in
inl [<hyps, if x then a else b fi >]
hyp => if concl ∈b hyps then inl [] else inr ⋅ fi
andE @i => if i <z ||hyps|| then let a,b = dest-"and"(hyps[i]) in inl [<[a; [b / hyps]], concl>] else inr ⋅ fi
orE @i => if i <z ||hyps|| then let a,b = dest-"or"(hyps[i]) in inl [<[a / hyps], concl>; <[b / hyps], concl>] e\000Clse inr ⋅ fi
impE @i => if i <z ||hyps|| then let a,b = dest-"imp"(hyps[i]) in inl [<hyps, a>; <[b / hyps], concl>] else inr \000C⋅ fi
allE @i with v => if i <z ||hyps|| ∧b v ∈b mFOL-sequent-freevars(<hyps, concl>)
then let x,b = dest-all(hyps[i]); in
inl [<[b[v/x] / hyps], concl>]
else inr ⋅
fi
existsE @i with v => if i <z ||hyps|| ∧b (¬bv ∈b mFOL-sequent-freevars(<hyps, concl>))
then let x,b = dest-exists(hyps[i]); in
inl [<[b[v/x] / hyps], concl>]
else inr ⋅
fi
falseE @i => if i <z ||hyps||
then let n,vars = dest-atomic(hyps[i]) in
if n =a "false" ∧b null(vars) then inl [] else inr ⋅ fi
else inr ⋅
fi
Lemma: FOLeffect_wf
∀[sr:mFOL-sequent() × FOLRule()]. (FOLeffect(sr) ∈ mFOL-sequent() List?)
Definition: mk_mFOLSequentRule
s BY r == <s, r>
Lemma: mk_mFOLSequentRule_wf
∀[s:mFOL-sequent()]. ∀[r:FOLRule()]. (s BY r ∈ mFOL-sequent() × FOLRule())
Definition: mk_mFOLProofNode
sr
subgoals == <sr, subgoals>
Lemma: mk_mFOLProofNode_wf
∀[T:Type]. ∀[sr:mFOL-sequent() × FOLRule()]. ∀[subgoals:T List]. (sr
subgoals ∈ mFOL-sequent() × FOLRule() × (T List))
Definition: mFOL-proveable
Provability of mFOL() sequent s.⋅
mFOL-proveable(s) == proveable(mFOL-sequent();FOLRule();λsr.mFOLeffect(sr);s)
Lemma: mFOL-proveable_wf
∀[s:mFOL-sequent()]. (mFOL-proveable(s) ∈ ℙ)
Definition: FOL-proveable
FOL-proveable(s) == proveable(mFOL-sequent();FOLRule();λsr.FOLeffect(sr);s)
Lemma: FOL-proveable_wf
∀[s:mFOL-sequent()]. (FOL-proveable(s) ∈ ℙ)
Definition: mFOL-proveable-formula
mFOL-proveable-formula(fmla) == mFOL-proveable(<[], fmla>)
Lemma: mFOL-proveable-formula_wf
∀[fmla:mFOL()]. (mFOL-proveable-formula(fmla) ∈ ℙ)
Definition: FOL-proveable-formula
FOL-proveable-formula(fmla) == FOL-proveable(<[], fmla>)
Lemma: FOL-proveable-formula_wf
∀[fmla:mFOL()]. (FOL-proveable-formula(fmla) ∈ ℙ)
Lemma: mFOL-proveable-evidence
Soundness theorem for mFOL() with respect to uniform evidence semantics.
It says that from a correct proof of a mFOL sequent we may construct
uniform evidence mFOL-sequent-evidence for the sequent.
Uniform evidence for an abstract formula, fmla, is the
intersection over all domains, Dom, and all structures, S, over Dom,
of evidence for ∀a:FOAssignment(vs,Dom). Dom,S,a |= fmla
where vs is the list of free variables of the formula.
NOTE:
If the formula is closed (i.e. the free vars is the nil list) then
an assignment a:FOAssignment([],Dom) exists even when Dom is an empty type..
Thus, (forall x. P(x)) => (exists x. P(x)) is not uniformly valid
because the premise is true for an empty domain while the conclusion is not.
By the soundness theorem, it is not provable.
By examining the effect of the mFOL rules
(see mFOLeffect)
one can see why this is so:
both forall elimination and exists introduction
can only be used with a variable already free in the sequent,
so there is no way to use either rule in a proof of this formula.⋅
∀[s:mFOL-sequent()]. (mFOL-proveable(s) ⇒ mFOL-sequent-evidence(s))
Lemma: FOStruct-false-subtype-evidence
∀Dom:Type. ∀S:FOStruct+{i:l}(Dom). ∀fmla:mFOL(). ∀a:FOAssignment(mFOL-freevars(fmla),Dom).
((S "false" []) ⊆r Dom,S,a +|= FOL-abstract(fmla))
Lemma: FOL-sequent-evidence-false-hyp
Uniform evidence for a trivially true sequent where the conclusion is
a given member of the hypotheses.⋅
∀hyps:mFOL() List. ∀concl:mFOL(). ∀i:ℕ||hyps||.
((↑mFOatomic?(hyps[i]))
⇒ (mFOatomic-name(hyps[i]) = "false" ∈ Atom)
⇒ (mFOatomic-vars(hyps[i]) = [] ∈ (ℤ List))
⇒ FOL-sequent-evidence{i:l}(<hyps, concl>))
Lemma: FOL-proveable-evidence
Soundness theorem for mFOL() with respect to uniform evidence semantics.
It says that from a correct proof of a mFOL sequent we may construct
uniform evidence mFOL-sequent-evidence for the sequent.
Uniform evidence for an abstract formula, fmla, is the
intersection over all domains, Dom, and all structures, S, over Dom,
of evidence for ∀a:FOAssignment(vs,Dom). Dom,S,a |= fmla
where vs is the list of free variables of the formula.
NOTE:
If the formula is closed (i.e. the free vars is the nil list) then
an assignment a:FOAssignment([],Dom) exists even when Dom is an empty type..
Thus, (forall x. P(x)) => (exists x. P(x)) is not uniformly valid
because the premise is true for an empty domain while the conclusion is not.
By the soundness theorem, it is not provable.
By examining the effect of the mFOL rules
(see mFOLeffect)
one can see why this is so:
both forall elimination and exists introduction
can only be used with a variable already free in the sequent,
so there is no way to use either rule in a proof of this formula.⋅
∀[s:mFOL-sequent()]. (FOL-proveable(s) ⇒ FOL-sequent-evidence{i:l}(s))
Lemma: mFOL-proveable-formula-evidence
Main Lemma. See mFOL-proveable-evidence also.⋅
∀[fmla:mFOL()]. (mFOL-proveable-formula(fmla) ⇒ mFOL-evidence(fmla))
Lemma: mFOL-proveable-formula-evidence-ext
Main Lemma. See mFOL-proveable-evidence also.⋅
∀[fmla:mFOL()]. (mFOL-proveable-formula(fmla) ⇒ mFOL-evidence(fmla))
Lemma: mFOL-proveable-formula-evidence-ext2
Main Lemma. See mFOL-proveable-evidence also.⋅
∀[fmla:mFOL()]. (mFOL-proveable-formula(fmla) ⇒ mFOL-evidence(fmla))
Lemma: mFOL-proveable-formula-evidence-ext3
Main Lemma. See mFOL-proveable-evidence also.⋅
∀[fmla:mFOL()]. (mFOL-proveable-formula(fmla) ⇒ mFOL-evidence(fmla))
Definition: new-mFO-var
new-mFO-var(H) ==
accumulate (with value m and list item fmla):
let vs ⟵ mFOL-freevars(fmla)
in eval n = bigger-int(m;vs) in
n
over list:
H
with starting value:
0)
Lemma: new-mFO-var_wf
∀[H:mFOL() List]. (new-mFO-var(H) ∈ ℤ)
Definition: compute-in-context
compute-in-context(constants;functions;t) ==
fix((λcompute-in-context,t. (if t is stopped at f,n then
case apply-alist(IntDeq;constants;n)
of inl(x) =>
compute-in-context (f x)
| inr(z) =>
case apply-alist(IntDeq;functions;n)
of inl(table) =>
(if f (λx.stop(x)) is stopped at g,arg then
if compute-in-context arg is an integer
case apply-alist(IntDeq;table;compute-in-context arg)
of inl(z) =>
compute-in-context (f (λx.z))
| inr(z) =>
t
else t
otherwise x.t)
| inr(z) =>
t
otherwise x.x)))
t
Definition: elimination-step
elimination-step(H;eliminated;model;f;n) ==
fix((λelimination-step,f,n. mFOL_ind(H[||H|| - n + 1];
mFOatomic(P,vars)⇒ "stopped on a atomic hyp??";
mFOconnect(knd,A,B)⇒ a,b.if knd =a "imp"
then (if f (λx.stop(x)) is stopped at g,a then
<n, a>
otherwise x.<n, "stopped on implies not applied??">)
else <n, 0>
fi ;
mFOquant(isall,v,body)⇒ r.if isall
then (if f (λx.stop(x)) is stopped at h,a then
(if compute-in-context(eliminated;model;a) is stopped at g,m then
elimination-step g m
otherwise b.<n, b>)
otherwise x.<n, "stopped on all not applied??">)
else <n, 0>
fi ) ))
f
n
Definition: do-elimination-step
do-elimination-step(H; G; eliminated; model; evd; f; n) ==
let incurrent = λe.<e, eliminated, model> in
let m,a = elimination-step(H;eliminated;model;f;n)
in let eliminate = λt.<evd, [<m, t> / eliminated], model> in
eval k = ||H|| in
eval hnum = k - m + 1 in
eval hyp = H[hnum] in
mFOL_ind(hyp;
mFOatomic(P,vars)⇒ "stopped on a atomic hyp??";
mFOconnect(knd,A,B)⇒ _,__.if knd =a "imp"
then <impE on hnum, [incurrent a; eliminate (λx.stop(k))]>
if knd =a "and" then <andE on hnum, [eliminate <stop(k + 1), stop(k)>]>
if knd =a "or" then <orE on hnum, [eliminate (inl stop(k)); eliminate (inr stop(k) )]>
else "funny connective??"
fi ;
mFOquant(isall,v,body)⇒ _.if isall
then eval model' = update-alist(IntDeq;model;m;[<a, stop(k)>];table.[<a, stop(k)> / table]) in
<allE on hnum with a, [<evd, eliminated, model'>]>
else eval j = new-mFO-var([G / H]) in
<existsE on hnum with j, [eliminate <j, stop(k)>]>
fi )
Definition: full-evd-proof-step
full-evd-proof-step:
sequent;
fullevd ==
let H,G = sequent
in let evd,eliminated,model = fullevd in
(if compute-in-context(eliminated;model;evd) is stopped at f,n then
if eq_term(f; λx.x) then <hyp, []> else do-elimination-step(H; G; eliminated; model; evd; f; n) fi
otherwise evd.let incurrent = λe.<e, eliminated, model> in
if evd is a pair
then let left,right = evd
in if mFOconnect?(G) ∧b mFOconnect-knd(G) =a "and"
then <andI, [incurrent left; incurrent right]>
else (if compute-in-context(eliminated;model;left) is stopped at f,n then
do-elimination-step(H; G; eliminated; model; evd; f; n)
otherwise w.<existsI with w, [incurrent right]>)
fi otherwise if evd is lambda then if mFOconnect?(G) ∧b mFOconnect-knd(G) =a "imp"
then eval k = ||H|| in
<impI, [incurrent (evd stop(k))]>
else eval m = new-mFO-var(H) in
<allI with new-mFO-var(H), [incurrent (evd m)]>
fi otherwise if evd is inl then <orI left, [incurrent outl(evd)]>
else if evd is inr then <orI right, [incurrent outr(evd)]>
else "can't happen if evd is correct")
Definition: uniform-evd-proof-checks
uniform-evd-proof-checks(sequent;fullevd) ==
fix((λuniform-evd-proof-checks,sequent,fullevd. let rule,subevd = full-evd-proof-step:
sequent;
fullevd
in let sr ⟵ <sequent, rule>
in case mFOLeffect(sr)
of inl(L) =>
let subgoals ⟵ L
in eval n = ||subgoals|| in
(∀i∈upto(n).uniform-evd-proof-checks subgoals[i] subevd[i])_b
| inr(z) =>
ff))
sequent
fullevd
Definition: uniform-evd-proof
uniform-evd-proof(sequent;fullevd) ==
fix((λuniform-evd-proof,sequent,fullevd. let rule,subevd = full-evd-proof-step:
sequent;
fullevd
in let sr ⟵ <sequent, rule>
in let subgoals ⟵ outl(mFOLeffect(sr))
in eval n = ||subgoals|| in
<sr, map(λi.(uniform-evd-proof subgoals[i] subevd[i]);upto(n))>))
sequent
fullevd
Definition: mfol-context
This is the list of hypotheses of a mFOL-sequent() in reverse order.⋅
mfol-context() == mFOL() List
Lemma: mfol-context_wf
mfol-context() ∈ Type
Definition: mfol-context-model
A pair <consts,funs> where consts is an association list that can assign
number n a triple such as ⌜<"pair", i, j>⌝.
funs is an association list of type ⌜(ℤ × ((ℤ × ℤ) List)) List⌝.
It can assign to number n a secondary association list.
So if 0 is assigned the list [<1,4>;<2;5>] it means that
0 is a function that maps domain element 1 to hypothesis 4 and
domain element 2 to hypothesis 5⋅
mfol-context-model() == (ℕ × Atom × ℕ × ℕ) List × ((ℕ × ((ℕ × ℕ) List)) List)
Lemma: mfol-context-model_wf
mfol-context-model() ∈ Type
Definition: context-lookup
context-lookup(Gamma;x) == Gamma[||Gamma|| - x + 1]
Lemma: context-lookup_wf
∀[Gamma:mFOL() List]. ∀[x:ℕ||Gamma||]. (context-lookup(Gamma;x) ∈ mFOL())
Lemma: context-lookup-stable1
∀[Gamma,more:mFOL() List]. ∀[x:ℕ||Gamma||]. (context-lookup(more @ Gamma;x) ~ context-lookup(Gamma;x))
Definition: consistent-model-const
consistent-model-const(Gamma;c) ==
let x,lbl,i,j = c
in x < ||Gamma||
∧ let H = context-lookup(Gamma;x) in
if lbl =a "function"
then ((↑mFOconnect?(H)) ∧ (¬(mFOconnect-knd(H) = "and" ∈ Atom)) ∧ (¬(mFOconnect-knd(H) = "or" ∈ Atom)))
∨ ((↑mFOquant?(H)) ∧ mFOquant-isall(H) = tt)
if lbl =a "pair"
then i < ||Gamma||
∧ j < ||Gamma||
∧ (↑mFOconnect?(H))
∧ (mFOconnect-knd(H) = "and" ∈ Atom)
∧ (mFOconnect-left(H) = context-lookup(Gamma;i) ∈ mFOL())
∧ (mFOconnect-right(H) = context-lookup(Gamma;j) ∈ mFOL())
if lbl =a "dpair"
then j < ||Gamma||
∧ (↑mFOquant?(H))
∧ mFOquant-isall(H) = ff
∧ (mFOquant-body(H)[i/mFOquant-var(H)] = context-lookup(Gamma;j) ∈ mFOL())
if lbl =a "inl"
then i < ||Gamma||
∧ (↑mFOconnect?(H))
∧ (mFOconnect-knd(H) = "or" ∈ Atom)
∧ (mFOconnect-left(H) = context-lookup(Gamma;i) ∈ mFOL())
if lbl =a "inr"
then i < ||Gamma||
∧ (↑mFOconnect?(H))
∧ (mFOconnect-knd(H) = "or" ∈ Atom)
∧ (mFOconnect-right(H) = context-lookup(Gamma;i) ∈ mFOL())
else True
fi
Lemma: consistent-model-const_wf
∀[Gamma:mFOL() List]. ∀[c:ℕ × Atom × ℕ × ℕ]. (consistent-model-const(Gamma;c) ∈ ℙ)
Lemma: consistent-model-const-stable
∀Gamma,more:mFOL() List. ∀c:ℕ × Atom × ℕ × ℕ.
(consistent-model-const(Gamma;c) ⇒ consistent-model-const(more @ Gamma;c))
Definition: consistent-model-fun
consistent-model-fun(Gamma;x;L) ==
x < ||Gamma||
∧ let H = context-lookup(Gamma;x) in
((↑mFOquant?(H))
∧ mFOquant-isall(H) = tt
∧ (∀p∈L.let i,j = p
in j < ||Gamma|| ∧ (mFOquant-body(H)[i/mFOquant-var(H)] = context-lookup(Gamma;j) ∈ mFOL())))
∨ ((↑mFOconnect?(H))
∧ (¬(mFOconnect-knd(H) = "and" ∈ Atom))
∧ (¬(mFOconnect-knd(H) = "or" ∈ Atom))
∧ (∀p∈L.let i,j = p
in i < ||Gamma||
∧ j < ||Gamma||
∧ (mFOconnect-left(H) = context-lookup(Gamma;i) ∈ mFOL())
∧ (mFOconnect-right(H) = context-lookup(Gamma;j) ∈ mFOL())))
Lemma: consistent-model-fun_wf
∀[Gamma:mFOL() List]. ∀[x:ℕ]. ∀[L:(ℕ × ℕ) List]. (consistent-model-fun(Gamma;x;L) ∈ ℙ)
Lemma: consistent-model-fun-stable
∀Gamma,more:mFOL() List. ∀x:ℕ. ∀L:(ℕ × ℕ) List.
(consistent-model-fun(Gamma;x;L) ⇒ consistent-model-fun(more @ Gamma;x;L))
Definition: consistent-context-model
consistent-context-model(Gamma;M) ==
let consts,funs = M
in (∀c∈consts.consistent-model-const(Gamma;c)) ∧ (∀f∈funs.let x,L = f in consistent-model-fun(Gamma;x;L))
Lemma: consistent-context-model_wf
∀[Gamma:mFOL() List]. ∀[M:mfol-context-model()]. (consistent-context-model(Gamma;M) ∈ ℙ)
Lemma: consistent-context-model-stable
∀Gamma,more:mFOL() List. ∀M:mfol-context-model().
(consistent-context-model(Gamma;M) ⇒ consistent-context-model(more @ Gamma;M))
Definition: modelEval
modelEval(exname;M;n)
==r let consts,funs = M
in case apply-alist(IntDeq;funs;n)
of inl(lst) =>
λi.if i is an integer then case apply-alist(IntDeq;lst;i)
of inl(j) =>
modelEval(exname;M;j)
| inr(x) =>
exception(exname; <n, i>)
else exception(exname; <n, i>)
| inr(x) =>
case apply-alist(IntDeq;consts;n)
of inl(x) =>
let lbl,i,j = x in
if lbl =a "function" then λx.exception(<exname, n, x>)
if lbl =a "pair" then <modelEval(exname;M;i), modelEval(exname;M;j)>
if lbl =a "dpair" then <i, modelEval(exname;M;j)>
if lbl =a "inl" then inl modelEval(exname;M;i)
if lbl =a "inr" then inr modelEval(exname;M;i)
if lbl =a "const" then λx.modelEval(exname;M;i)
else exception(exname; n)
fi
| inr(x) =>
exception(exname; n)
Definition: modelAdd
M[n:= lbl,i,j] == let consts,funs = M in <update-alist(IntDeq;consts;n;<lbl, i, j>;tr.<lbl, i, j>), funs>
Definition: modelUpdate
M[fnum(x) :=n] == let consts,funs = M in <consts, update-alist(IntDeq;funs;fnum;[<x, n>];l.[<x, n> / l])>
Definition: note-is-function
note-is-function(A;hnum;M) == if mFOLisImp(A) ∨bmFOLisAll(A) then M[hnum:= `function`] else M fi
Definition: ex-do-Intro
ex-do-Intro(exname; H; G; numhyps; val; fullevd) ==
let F,M = fullevd
in mFOL_ind(G;
mFOatomic(P,vars)⇒ "should not happen??";
mFOconnect(knd,A,B)⇒ _,__.if knd =a "imp"
then let M' ⟵ note-is-function(A;numhyps;M)
in <impI, [<λM.(F M modelEval(exname;M;numhyps)), M'>]>
if knd =a "and" then <andI, [<λM.(fst((F M))), M>; <λM.(snd((F M))), M>]>
if knd =a "or"
then case val of inl(_) => <orI left, [<λM.outl(F M), M>]> | inr(_) => <orI right, [<λM.outr(F M), M>]>
else "funny connective??"
fi ;
mFOquant(isall,v,body)⇒ _.if isall
then eval m = new-mFO-var(H) in
<allI with m, [<λM.(F M m), M>]>
else eval j = fst(val) in
<existsI with j, [<λM.(snd((F M))), M>]>
fi )
Definition: ex-do-Elim
In the case for impE (implies elimination)
we update the function F to
λM.F M?exname:e.if e is a pair then let a,b = e
in if (a =z m) then b else exception(exname; e) fi otherwise exception(exname; e)
That is bad because it introduces a catch of the exception.
Why can't we simply use λM.(snd(m')) ?
It doesn't work for the example ⌜<¬(¬(P ∨ ¬(P))), λh.(h (inr (λx.(h (inl x))) ))>⌝
Why that is can be seen by comparing
proof-generation-for-example-5 and alt-proof-generation-for-example-5
I think we need to use
λM.F M?nnn:e.e
where nnn is a fresh name, and the model has been updated so that
ModelEval(M,m) = ⌜λx.(exception(nnn; x))⌝⋅
ex-do-Elim(exname;H;G;numhyps;m';fullevd)
==r let F,M = fullevd
in eval m = if m' is a pair then fst(m') otherwise m' in
eval hnum = numhyps - m + 1 in
eval hyp = H[hnum] in
mFOL_ind(hyp;
mFOatomic(P,vars)⇒ if deq-mFO() G P(vars) then <hyp, []> else <falseE on hnum, []> fi ;
mFOconnect(knd,A,B)⇒ _,__.if knd =a "imp"
then let M' ⟵ note-is-function(B;numhyps;M[m:= λx.numhyps])
in <impE on hnum
, [<λM.F M?exname:e.if e is a pair
then let a,b = e
in if (a =z m)
then b
else exception(exname; e)
fi otherwise exception(exname; e)
, M
>;
<F, M'>]
>
if knd =a "and"
then let M' ⟵ note-is-function(A;numhyps + 1;note-is-function(B;numhyps;M[m:= <numhyps
+ 1,numhyps>]))
in <andE on hnum, [<F, M'>]>
if knd =a "or"
then let M1 ⟵ note-is-function(A;numhyps;M[m:= inl(numhyps)])
in let M2 ⟵ note-is-function(B;numhyps;M[m:= inr(numhyps)])
in <orE on hnum, [<F, M1>; <F, M2>]>
else "funny connective??"
fi ;
mFOquant(isall,v,body)⇒ _.if isall
then eval a = snd(m') in
let M' ⟵ note-is-function(body;numhyps;M[m(a) :=numhyps])
in <allE on hnum with a, [<F, M'>]>?exname:m'.ex-do-Elim(exname;H;G;numhyps;m';fullevd)
else eval j = new-mFO-var([G / H]) in
let M' ⟵ note-is-function(body;numhyps;M[m:= <dj,numhyps>])
in <existsE on hnum with j, [<F, M'>]>
fi )
Definition: ex-evd-proof-step
ex-evd-proof-step(exname; sequent; fullevd) ==
let H,G = sequent
in eval numhyps = ||H|| in
let F,M = fullevd
in eval v = F M in
ex-do-Intro(exname; H; G; numhyps; v; fullevd)?exname:n.ex-do-Elim(exname;H;G;numhyps;n;fullevd)
Definition: list-to-fun
list-to-fun(L) == λi.L[i]
Lemma: list-to-fun_wf
∀[T:Type]. ∀[L:T List]. (list-to-fun(L) ∈ ℕ||L|| ⟶ T)
Definition: ex-evd-proof
ex-evd-proof(exname;sequent;F)
==r let rule,subevd = ex-evd-proof-step(exname; sequent; F)
in let sr ⟵ <sequent, rule>
in let subgoals ⟵ outl(FOLeffect(sr))
in eval n = ||subgoals|| in
let L ⟵ map(λi.ex-evd-proof(exname;subgoals[i];subevd[i]);upto(n))
in <sr, L>
Definition: ex-evd-proof-check
ex-evd-proof-check(exname;sequent;F)
==r let rule,subevd = ex-evd-proof-step(exname; sequent; F)
in let sr ⟵ <sequent, rule>
in case mFOLeffect(sr)
of inl(subgoals) =>
eval n = ||subgoals|| in
(∀i∈upto(n).ex-evd-proof-check(exname;subgoals[i];subevd[i]))_b
| inr(z) =>
ff
Definition: list_proof_to_W_proof
list_proof_to_W_proof(p)
==r let sr,subgoals = p
in let L ⟵ map(λp.list_proof_to_W_proof(p);subgoals)
in <sr, list-to-fun(L)>
Definition: uniform-evd-to-proof
uniform-evd-to-proof(G;evd) == let p ⟵ ν(ex.ex-evd-proof(ex;<[], G>;<λM.evd, [], []>)) in p
Definition: uniform-evd-proof-check
uniform-evd-proof-check(exname; fmla; evd) == evalall(ex-evd-proof-check(exname;<[], fmla>;<λM.evd, [], []>))
Comment: the proof algorithm
Starting with evidence evd of formula G, we form sequent ⌜<[], G>⌝
and "full evidence" ⌜<λM.evd, [], []>⌝ consisting of function F = ⌜λM.evd⌝
and the empty model M = <[], []>.
We also need a name ⌜exname⌝ that is fresh w.r.t. the evidence (i.e. not mentioned in evd).
uniform-evd-to-proof(exname; G; evd) == evalall(ex-evd-proof(exname;<[], G>;<λM.evd, [], []>))
To generate the proof of a sequent from its full evidence, we generate the next step
consisting of the proof rule to apply and a list of full evidence for the subgoals.
The minimal-first-order-logic proof system defines the effect of the rule r on sequent s
as either ⌜inl subgoals⌝ or ⌜inr Ax ⌝ where the rule succeeds when we get ⌜inl subgoals⌝.
So we build the proof tree by putting in the sequent and rule and the list of subproofs
generated by pairing up the subgoal sequents with the sub-evidence.
ex-evd-proof(exname;sequent;fullevd)
==r let rule,subevd = ex-evd-proof-step(exname; sequent; fullevd)
in let sr ⟵ <sequent, rule>
in let subgoals ⟵ outl(mFOLeffect(sr))
in eval n = ||subgoals|| in
<sr, map(λi.ex-evd-proof(subgoals[i]; subevd[i]);upto(n))>
To generate the next step apply the function F to the model M.
If we get a value, do an introduction rule,
if an exception is raised
(either when F is applied to M, or when computing the introduction rule),
then catch that exception and do an elimination step.
ex-evd-proof-step(exname; sequent; fullevd) ==
let H,G = sequent
in eval numhyps = ||H|| in
let F,M = fullevd
in eval v = F M in
ex-do-Intro(exname; H; G; numhyps; v; fullevd)?exname:n.ex-do-Elim(exname;H;G;numhyps;n;fullevd)
To do an introduction rule using the value, val, computed from the evidence,
do a case analysis on the conclusion G of the sequent.
The only case that adds a new hypothesis is implies introduction.
In that case, we update the model M when the new hypothesis A is a function
(a forall formula or an implies formula) to indicate that.
Otherwise the model M stays the same.
The function F that we apply to the model is updated so that it applies
the appropriate operation (e.g. fst, snd, outl, outr) to the previously computed (F M).
In the case of exists, we compute the first component of the pair, val.
If that raises an exception, then the introduction step will raise an exception and
the proof will do an elimination step instead.
Notice that the ImpliesIntroduction changes the function so that it applies the evidence to
another argument, modelEval(M,n), where n = numhyps is the number of
the newly introduced hypothesis.
The definition of modelEval is given below (at the end).
ex-do-Intro(H;G;numhyps;val;fullevd) ==
let F,M = fullevd
in mFOL_ind(G;
mFOatomic(P,vars)⇒ "should not happen??";
mFOconnect(knd,A,B)⇒ _,__.if knd =a "imp"
then let M' ⟵ note-is-function(A;numhyps;M)
in <impI, [<λM.(F M modelEval(M; numhyps)), M'>]>
if knd =a "and" then <andI, [<λM.(fst((F M))), M>; <λM.(snd((F M))), M>]>
if knd =a "or"
then case val of inl(_) => <orI left, [<λM.outl(F M), M>]> | inr(_) => <orI right, [<λM.outr(F M), M>]>
else "funny connective??"
fi ;
mFOquant(isall,v,body)⇒ _.if isall
then eval m = new-mFO-var(H) in
<allI with m, [<λM.(F M m), M>]>
else eval j = fst(val) in
<existsI with j, [<λM.(snd((F M))), M>]>
fi )
Here is the definition of note-is-function:
note-is-function(A;hnum;M) == if mFOLisImp(A) ∨bmFOLisAll(A) then M[hnum:= `function`] else M fi
To do an elimination step using the exception m', we use the first
component m of m' when m' is a pair.
That is because when we evaluate hypothesis number m in a model that only
specifies that m is a function, then we use ⌜λx.exception(<exname, m, x>)⌝
for the meaning of m. That will raise a (named) exception with value part
⌜<m, x>⌝ if the function is applied to term ⌜x⌝ in a principal part
of the computation, and we will
know that hypothesis m needs elimination and that it was applied to term x.
From m, we get the hypothesis on which to apply the elimination rule (the hypotheses are listed in
reverse H(numhyps-1),...., H2, H1, H0 ) and do case analysis on that hypothesis.
In most cases, in the evidence for the generated subgoal(s),
the function F in the full evidence stays the same, and the model is updated.
The model is updated to indicate that, for example, an "and" hypothesis is equal to the
pair of new hypotheses, or an "or" hypothesis is equal to inl or inr of the new hypothesis.
In every case that adds a new hypothesis, we use note-is-function to update the model when the
new hypothesis is a function.
The trickiest case is the evidence for the first subgoal of implies-elimination.
In that case we know that the computation (F M) raises exception ⌜<m, x>⌝ so we change the
function so that it catches exceptions and when the exception has the form ⌜<m, x>⌝ it continues
using evidence x. It re-raises any other exceptions.
The other tricky case is forall-elimination.
In that case, since a forall is a function,
the exception m' must be a pair, and the second component
is the domain element to be instantiated.
So we try to compute that to a value.
If an exception is raised, then we use that to compute the
next step instead.
Because of that possibilty, the function ex-do-Elim is recursive.
%---%
ex-do-Elim(exname;H;G;numhyps;m';fullevd)
==r let F,M = fullevd
in eval m = if m' is a pair then fst(m') otherwise m' in
eval hnum = numhyps - m + 1 in
eval hyp = H[hnum] in
mFOL_ind(hyp;
mFOatomic(P,vars)⇒ <hyp, []>;
mFOconnect(knd,A,B)⇒ _,__.if knd =a "imp"
then let M' ⟵ note-is-function(B;numhyps;M[m:= λx.numhyps])
in <impE on hnum
, [<λM.F M?exname:e.if e is a pair then let a,b = e
in if (a =z m)
then b
else exception(<exname
, e
>)
fi
otherwise exception(<exname, e>)
, M
>;
<F, M'>]
>
if knd =a "and"
then let M' ⟵ note-is-function(A;numhyps + 1;note-is-function(B;numhyps;M[m:= <numhyps
+ 1,numhyps>]))
in <andE on hnum, [<F, M'>]>
if knd =a "or"
then let M1 ⟵ note-is-function(A;numhyps;M[m:= inl(numhyps)])
in let M2 ⟵ note-is-function(B;numhyps;M[m:= inr(numhyps)])
in <orE on hnum, [<F, M1>; <F, M2>]>
else "funny connective??"
fi ;
mFOquant(isall,v,body)⇒ _.if isall
then eval a = snd(m') in
let M' ⟵ note-is-function(body;numhyps;M[m(a) :=numhyps])
in <allE on hnum with a, [<F, M'>]>?exname:m'.ex-do-Elim(exname;H;G;numhyps;m';fullevd)
else eval j = new-mFO-var([G / H]) in
let M' ⟵ note-is-function(body;numhyps;M[m:= <dj,numhyps>])
in <existsE on hnum with j, [<F, M'>]>
fi )
Finally, here is the recursive definition of modelEval(M,n):
M is a pair <consts,funs> where consts is an association list of type
⌜(ℤ × Atom × ℤ × ℤ) List⌝ that can assign to number n a triple such as ⌜<"pair", i, j>⌝.
funs is an association list of type ⌜(ℤ × ((ℤ × ℤ) List)) List⌝. It can assign to number n
a secondary association list. So if 0 is assigned the list [<1,4>;<2;5>] it means that
0 is a function that maps domain element 1 to hypothesis 4 and domain element 2 to hypothesis 5.
modelEval(exname;M;n)
==r let consts,funs = M
in case apply-alist(IntDeq;funs;n)
of inl(lst) =>
λi.if i is an integer then case apply-alist(IntDeq;lst;i)
of inl(j) =>
modelEval(exname;M;j)
| inr(x) =>
exception(<exname, n, i>)
else exception(<exname, n, i>)
| inr(x) =>
case apply-alist(IntDeq;consts;n)
of inl(x) =>
let lbl,i,j = x in
if lbl =a "function" then λx.exception(<exname, n, x>)
if lbl =a "pair" then <modelEval(exname;M;i), modelEval(exname;M;j)>
if lbl =a "dpair" then <i, modelEval(exname;M;j)>
if lbl =a "inl" then inl modelEval(exname;M;i)
if lbl =a "inr" then inr modelEval(exname;M;i)
if lbl =a "const" then λx.modelEval(exname;M;i)
else exception(<exname, n>)
fi
| inr(x) =>
exception(<exname, n>)⋅
Comment: proof-generation-for-example-5
We are proving ⌜¬(¬(P ∨ ¬(P)))⌝ with evidence ⌜λh.(h (inr (λx.(h (inl x))) ))⌝.
Since the evidence is a lambda, the first step is impI
which gives H = [¬(P ∨ ¬(P))], G = False,
M = ⌜<<<0, "function", 0, 0>, Ax>, Ax>⌝
F = ⌜λM.((λM,h. (h (inr (λx.(h (inl x))) ))) M modelEval("xx";M;0))⌝
F M computes to ⌜exception("xx"; <0, inr (λx.(modelEval("xx";<<<0, "function", 0, 0>, Ax>, Ax>;0) (inl x))) >)⌝
so the next step is ⌜impE on 0⌝
In the first subgoal we have
H = [¬(P ∨ ¬(P))], G = P ∨ ¬(P)
M = ⌜<<<0, "function", 0, 0>, Ax>, Ax>⌝
F = ⌜λM.(λM.((λM,h. (h (inr (λx.(h (inl x))) ))) M modelEval("xx";M;0))) M?"xx":e.if e is a pair
then let a,b = e
in if (a =z 0)
then b
else exception("xx"; e)
fi
otherwise exception("xx"; e)⌝
The second subgoal has
H = [False; ¬(P ∨ ¬(P))], G = False
M = ⌜<<<0, "const", 1, 0>, Ax>, Ax>⌝
F = ⌜λM.((λM,h. (h (inr (λx.(h (inl x))) ))) M modelEval("xx";M;0))⌝
Here F M computes to ⌜exception("xx"; 1)⌝ so we generate Hyp 1.
Back in the first subgoal, F M computes to
⌜inr (λx.(modelEval("xx";<<<0, "function", 0, 0>, Ax>, Ax>;0) (inl x))) ⌝
so the next rule is ⌜orI right⌝
H = [¬(P ∨ ¬(P))], G = ¬(P)
M = ⌜<<<0, "function", 0, 0>, Ax>, Ax>⌝
F =
⌜λM.outr((λM.(λM.((λM,h. (h (inr (λx.(h (inl x))) ))) M modelEval("xx";M;0))) M?"xx":e.if e is a pair
then let a,b = e
in if (a =z 0)
then b
else exception("xx"; e)
fi
otherwise exception("xx"; e))
M)⌝
F M computes to ⌜λx.(modelEval("xx";<<<0, "function", 0, 0>, Ax>, Ax>;0) (inl x))⌝
so the next rule is ⌜impI⌝
and we get H = [P; ¬(P ∨ ¬(P))], G = False
M = ⌜<<<0, "function", 0, 0>, Ax>, Ax>⌝
F =
⌜λM.((λM.outr((λM.(λM.((λM,h. (h (inr (λx.(h (inl x))) ))) M modelEval("xx";M;0))) M?"xx":e.if e is a pair
then let a,b = e
in if (a =z 0)
then b
else exception("xx"; e)
fi
otherwise exception("xx"; e))
M))
M
modelEval("xx";M;1))⌝
%---%
F M computes to ⌜exception("xx"; <0, inl modelEval("xx";<<<0, "function", 0, 0>, Ax>, Ax>;1)>)⌝
so the next rule is ⌜impE on 1⌝ which generates two subgoals:
H = [P; ¬(P ∨ ¬(P))], G = P ∨ ¬(P)
M = ⌜<<<0, "function", 0, 0>, Ax>, Ax>⌝
F =
⌜λM.(λM.((λM.outr((λM.(λM.((λM,h. (h (inr (λx.(h (inl x))) ))) M modelEval("xx";M;0)))
M?"xx":e.if e is a pair then let a,b = e
in if (a =z 0) then b else exception("xx"; e) fi
otherwise exception("xx"; e))
M))
M
modelEval("xx";M;1)))
M?"xx":e.if e is a pair then let a,b = e
in if (a =z 0) then b else exception("xx"; e) fi otherwise exception("xx"; e)⌝
and H = [False; P; ¬(P ∨ ¬(P))], G = False
M = ⌜<<0, "const", 2, 0>, Ax>⌝
F =
⌜λM.((λM.(λM.((λM.outr((λM.(λM.((λM,h. (h (inr (λx.(h (inl x))) ))) M modelEval("xx";M;0)))
M?"xx":e.if e is a pair then let a,b = e
in if (a =z 0) then b else exception("xx"; e) fi
otherwise exception("xx"; e))
M))
M
modelEval("xx";M;1)))
M?"xx":e.if e is a pair then let a,b = e
in if (a =z 0) then b else exception("xx"; e) fi otherwise exception("xx"; e))
modelEval("xx";M;1))⌝
Here F M computes to ⌜exception("xx"; 1)⌝ so we generate Hyp
%---%
In the first subgoal, F M computes to ⌜inl modelEval("xx";<<<0, "function", 0, 0>, Ax>, Ax>;1)⌝
so the next step is ⌜orI left⌝
H = [P; ¬(P ∨ ¬(P))], G = P
M = ⌜<<<0, "function", 0, 0>, Ax>, Ax>⌝
F =
⌜λM.outl((λM.(λM.((λM.outr((λM.(λM.((λM,h. (h (inr (λx.(h (inl x))) ))) M modelEval("xx";M;0)))
M?"xx":e.if e is a pair then let a,b = e
in if (a =z 0) then b else exception("xx"; e) fi
otherwise exception("xx"; e))
M))
M
modelEval("xx";M;1)))
M?"xx":e.if e is a pair then let a,b = e
in if (a =z 0) then b else exception("xx"; e) fi
otherwise exception("xx"; e))
M)⌝
F M computes to ⌜exception("xx"; 1)⌝ so we generate Hyp
and the proof is finished.
⌜⊢ ¬(¬(P ∨ ¬(P)))
BY impI
¬(P ∨ ¬(P))
⊢ false
BY impE on 0
¬(P ∨ ¬(P)) ⊢ P ∨ ¬(P) BY orI right
¬(P ∨ ¬(P)) ⊢ ¬(P) BY impI
P, ¬(P ∨ ¬(P)) ⊢ false BY impE on 1
P, ¬(P ∨ ¬(P)) ⊢ P ∨ ¬(P) BY orI left
P, ¬(P ∨ ¬(P)) ⊢ P BY hyp, false, P, ¬(P ∨ ¬(P)) ⊢ false BY hyp, false, ¬(P ∨ ¬(P)) ⊢ false BY hyp⌝⋅
Comment: alt-proof-generation-for-example-5
Now we see where the alternate version for implies elimination goes
wrong for this example:
We are proving ⌜¬(¬(P ∨ ¬(P)))⌝ with evidence ⌜λh.(h (inr (λx.(h (inl x))) ))⌝.
Since the evidence is a lambda, the first step is impI
which gives H = [¬(P ∨ ¬(P))], G = False,
M = ⌜<<<0, "function", 0, 0>, Ax>, Ax>⌝
F = ⌜λM.((λM,h. (h (inr (λx.(h (inl x))) ))) M modelEval("xx";M;0))⌝
F M computes to ⌜exception("xx"; <0, inr (λx.(modelEval("xx";<<<0, "function", 0, 0>, Ax>, Ax>;0) (inl x))) >)⌝
so the next step is ⌜impE on 0⌝
In the first subgoal we have
H = [¬(P ∨ ¬(P))], G = P ∨ ¬(P)
M = ⌜<<<0, "function", 0, 0>, Ax>, Ax>⌝
F = ⌜λM.(snd(<0, inr (λx.(modelEval("xx";<<<0, "function", 0, 0>, Ax>, Ax>;0) (inl x))) >))⌝
The second subgoal has
H = [False; ¬(P ∨ ¬(P))], G = False
M = ⌜<<<0, "const", 1, 0>, Ax>, Ax>⌝
F = ⌜λM.((λM,h. (h (inr (λx.(h (inl x))) ))) M modelEval("xx";M;0))⌝
Here F M computes to ⌜exception("xx"; 1)⌝ so we generate Hyp 1.
Back in the first subgoal, F M computes to
⌜inr (λx.(modelEval("xx";<<<0, "function", 0, 0>, Ax>, Ax>;0) (inl x))) ⌝
so the next rule is ⌜orI right⌝
H = [¬(P ∨ ¬(P))], G = ¬(P)
M = ⌜<<<0, "function", 0, 0>, Ax>, Ax>⌝
F = ⌜λM.outr((λM.(snd(<0, inr (λx.(modelEval("xx";<<<0, "function", 0, 0>, Ax>, Ax>;0) (inl x))) >))) M)⌝
F M computes to ⌜λx.(modelEval("xx";<<<0, "function", 0, 0>, Ax>, Ax>;0) (inl x))⌝
so the next rule is ⌜impI⌝
and we get H = [P; ¬(P ∨ ¬(P))], G = False
M = ⌜<<<0, "function", 0, 0>, Ax>, Ax>⌝
F = ⌜λM.((λM.outr((λM.(snd(<0, inr (λx.(modelEval("xx";<<<0, "function", 0, 0>, Ax>, Ax>;0) (inl x))) >))) M)\000C) M
modelEval("xx";M;1))⌝
%---%
F M computes to ⌜exception("xx"; <0, inl modelEval("xx";<<<0, "function", 0, 0>, Ax>, Ax>;1)>)⌝
so the next rule is ⌜impE on 1⌝ which generates two subgoals:
H = [P; ¬(P ∨ ¬(P))], G = P ∨ ¬(P)
M = ⌜<<<0, "function", 0, 0>, Ax>, Ax>⌝
F = ⌜λM.(snd(<0, inl modelEval("xx";<<<0, "function", 0, 0>, Ax>, Ax>;1)>))⌝
and H = [False; P; ¬(P ∨ ¬(P))], G = False
M = ⌜<<0, "const", 2, 0>, Ax>⌝
F = ⌜λM.((λM.outr((λM.(snd(<0, inr (λx.(modelEval("xx";<<<0, "function", 0, 0>, Ax>, Ax>;0) (inl x))) >))) M)) M mo\000CdelEval("xx";M;1))⌝
Here F M does not computes to ⌜exception("xx"; 1)⌝ like it did before.
It computes to ⌜exception("xx"; <0, inl modelEval("xx";<<0, "const", 2, 0>, Ax>;1)>)⌝
(which makes us use ImpE again.)
The problem is that the model ⌜<<<0, "function", 0, 0>, Ax>, Ax>⌝ is in our F
but the current model is supposed to be ⌜<<0, "const", 2, 0>, Ax>⌝
%---%
In the first subgoal, F M computes to ⌜inl modelEval("xx";<<<0, "function", 0, 0>, Ax>, Ax>;1)⌝
so the next step is ⌜orI left⌝
H = [P; ¬(P ∨ ¬(P))], G = P
M = ⌜<<<0, "function", 0, 0>, Ax>, Ax>⌝
F = ⌜λM.outl((λM.(snd(<0, inl modelEval("xx";<<<0, "function", 0, 0>, Ax>, Ax>;1)>))) M)⌝
F M computes to ⌜exception("xx"; 1)⌝ so we generate Hyp
and the proof is finished.
⌜⊢ ¬(¬(P ∨ ¬(P)))
BY impI
¬(P ∨ ¬(P))
⊢ false
BY impE on 0
¬(P ∨ ¬(P)) ⊢ P ∨ ¬(P) BY orI right
¬(P ∨ ¬(P)) ⊢ ¬(P) BY impI
P, ¬(P ∨ ¬(P)) ⊢ false BY impE on 1
P, ¬(P ∨ ¬(P)) ⊢ P ∨ ¬(P) BY orI left
P, ¬(P ∨ ¬(P)) ⊢ P BY hyp, false, P, ¬(P ∨ ¬(P)) ⊢ false BY hyp, false, ¬(P ∨ ¬(P)) ⊢ false BY hyp⌝⋅
Comment: model as function
Instead of having a model be a pair of tables (for constants and functions)
and then having a (recursive) modelEval(M,x) function,
we can have the model itself be the function modelEval(M,x)
To do that, we have to combine the two tables into one function.
The first table associates numbers to values like <i,j> or inl k or "function"
and the second table was for things that
the first table said were "functions".
To handle this structure we need a function that can take as inputs
either numbers, n, of pairs of numbers <m,k>.
We start with the "undefined" model λx.(exception(exname; x))
and then "update" a given model function M to assign values to certain inputs.
For example, if we want to add that n = pair m k
then we make \x. if x = n then < M m, M k> else M x.
That updates the model M to add the new information and also builds in the
evaluation of M m and M k -- but only lazily.
To add the fact that n = "function" we make
M' = \x. if x = n then \i. M <n,i> else M x
So now M' n z = exception(exname, <n,z>)
-- if M does not have an update for <n,z>
To add an update like <n,k> = j we make
M' = \x. if x = <n,k> then M j else M x
So we need only these two kinds of updates
: compare input x with a given number n
: compare input x with a given pair of numbers <n,k>
To do that we use the canonical form tests
⌜if [z] is an integer then [a]
else [b]⌝
and ⌜if [z] is a pair then [a] otherwise [b]⌝
⋅
Definition: model-fun-update1
M[n:= m.F[m]] == λx.if x is an integer then if x=n then F[M] else (M x) else M x
Definition: update-fun
update-fun(M;A;hnum) == if mFOLisImp(A) ∨bmFOLisAll(A) then M[hnum:= m.λi.(m <hnum, i>)] else M fi
Definition: model-fun-update2
M[n,k := m.F[m]] ==
λx.if x is a pair then let y,z = x
in if y=n then if z=k then F[M] else (M x) else (M x) otherwise M x
Definition: fun-do-Intro
fun-do-Intro(exname;H;G;numhyps;val;fullevd) ==
let F,M = fullevd
in mFOL_ind(G;
mFOatomic(P,vars)⇒ "should not happen??";
mFOconnect(knd,A,B)⇒ _,__.if knd =a "imp"
then let M' ⟵ update-fun(M;A;numhyps)
in <impI, [<λM.(F M (M numhyps)), M'>]>
if knd =a "and" then <andI, [<λM.(fst((F M))), M>; <λM.(snd((F M))), M>]>
if knd =a "or"
then case val of inl(_) => <orI left, [<λM.outl(F M), M>]> | inr(_) => <orI right, [<λM.outr(F M), M>]>
else "funny connective??"
fi ;
mFOquant(isall,v,body)⇒ _.if isall
then eval m = new-mFO-var(H) in
<allI with m, [<λM.(F M m), M>]>
else eval j = fst(val) in
<existsI with j, [<λM.(snd((F M))), M>]>
fi )
Definition: fun-do-Elim
fun-do-Elim(exname;H;G;numhyps;m';fullevd)
==r let F,M = fullevd
in eval m = if m' is a pair then fst(m') otherwise m' in
eval hnum = numhyps - m + 1 in
eval hyp = H[hnum] in
mFOL_ind(hyp;
mFOatomic(P,vars)⇒ if deq-mFO() G P(vars) then <hyp, []> else <falseE on hnum, []> fi ;
mFOconnect(knd,A,B)⇒ _,__.if knd =a "imp"
then let M' ⟵ update-fun(M[m:= Md.λx.(Md numhyps)];B;numhyps)
in <impE on hnum
, [<λM.F M?exname:e.if e is a pair
then let a,b = e
in if (a =z m)
then b
else exception(exname; e)
fi otherwise exception(exname; e)
, M
>;
<F, M'>]
>
if knd =a "and"
then let M' ⟵ update-fun(update-fun(M[m:= Md.<Md (numhyps + 1), Md numhyps>];B;numhyps);A;numhyps +\000C 1)
in <andE on hnum, [<F, M'>]>
if knd =a "or"
then let M1 ⟵ update-fun(M[m:= Md.inl (Md numhyps)];A;numhyps)
in let M2 ⟵ update-fun(M[m:= Md.inr (Md numhyps) ];B;numhyps)
in <orE on hnum, [<F, M1>; <F, M2>]>
else "funny connective??"
fi ;
mFOquant(isall,v,body)⇒ _.if isall
then eval a = snd(m') in
let M' ⟵ update-fun(M[m,a := Md.Md numhyps];body;numhyps)
in <allE on hnum with a, [<F, M'>]>?exname:m'.fun-do-Elim(exname;H;G;numhyps;m';fullevd)
else eval j = new-mFO-var([G / H]) in
let M' ⟵ update-fun(M[m:= Md.<j, Md numhyps>];body;numhyps)
in <existsE on hnum with j, [<F, M'>]>
fi )
Definition: fun-evd-proof-step
fun-evd-proof-step(exname;sequent;fullevd) ==
let H,G = sequent
in eval numhyps = ||H|| in
let F,M = fullevd
in eval v = F M in
fun-do-Intro(exname;H;G;numhyps;v;fullevd)?exname:n.fun-do-Elim(exname;H;G;numhyps;n;fullevd)
Definition: fun-evd-proof
fun-evd-proof(exname;sequent;F)
==r let rule,subevd = fun-evd-proof-step(exname;sequent;F)
in let sr ⟵ <sequent, rule>
in let subgoals ⟵ outl(FOLeffect(sr))
in eval n = ||subgoals|| in
let L ⟵ map(λi.fun-evd-proof(exname;subgoals[i];subevd[i]);upto(n))
in <sr, L>
Definition: uniform-evd-proof
uniform-evd-proof(G;evd) == let p ⟵ ν(ex.fun-evd-proof(ex;<[], G>;<λM.evd, λx.(exception(ex; x))>)) in p
Definition: new-do-Intro
new-do-Intro(exname;H;G;numhyps;val;evd) ==
case(G)
P(vars) => "should not happen??";
A knd B => if knd =a "imp" then <impI, [λM.(evd M (M numhyps))]>
if knd =a "and" then <andI, [λM.(fst((evd M))); λM.(snd((evd M)))]>
if knd =a "or" then case val of inl(_) => <orI left, [λM.outl(evd M)]> | inr(_) => <orI right, [λM.outr(evd M)]>
else "funny connective??"
fi ;
isall v.body => if isall
then eval m = new-mFO-var(H) in
<allI with m, [λM.(evd M m)]>
else eval j = fst(val) in
<existsI with j, [λM.(snd((evd M)))]>
fi
Definition: new-do-Elim
new-do-Elim(exname;H;G;numhyps;m';evd)
==r eval m = if m' is a pair then fst(m') otherwise m' in
eval hnum = numhyps - m + 1 in
eval hyp = H[hnum] in
case(hyp)
P(vars) => if deq-mFO() G P(vars) then <hyp, []> else <falseE on hnum, []> fi ;
A knd B => if knd =a "imp"
then <impE on hnum
, [λM.evd M?exname:e.if e is a pair then let a,b = e
in if (a =z m) then b else exception(exname; e) fi
otherwise exception(exname; e);
λM.(evd (λi.if (i =z m) then λx.(M numhyps) else M i fi ))]
>
if knd =a "and" then <andE on hnum, [λM.(evd (λi.if (i =z m) then <M (numhyps + 1), M numhyps> else M i fi ))]>
if knd =a "or"
then <orE on hnum
, [λM.(evd (λi.if (i =z m) then inl (M numhyps) else M i fi ));
λM.(evd (λi.if (i =z m) then inr (M numhyps) else M i fi ))]
>
else "funny connective??"
fi ;
isall v.body => if isall
then eval a = snd(m') in
<allE on hnum with a
, [λM.(evd (λi.if (i =z m) then λx.if (x =z a) then M numhyps else M i x fi else M i fi ))]
>?exname:m'.new-do-Elim(exname;H;G;numhyps;m';evd)
else eval j = new-mFO-var([G / H]) in
<existsE on hnum with j, [λM.(evd (λi.if (i =z m) then <j, M numhyps> else M i fi ))]>
fi
Definition: probe
probe(H;exname) ==
eval numhyps = ||H|| in
λi.eval hnum = numhyps - i + 1 in
eval hyp = H[hnum] in
if (mFOconnect?(hyp) ∧b mFOconnect-knd(hyp) =a "imp") ∨b(mFOquant?(hyp) ∧b mFOquant-isall(hyp))
then λx.(exception(exname; <i, x>))
else exception(exname; i)
fi
Definition: new-evd-proof-step
NewEvdProofStep(exname;sequent;evd) ==
let H,G = sequent
in eval numhyps = ||H|| in
eval v = evd probe(H;exname) in
new-do-Intro(exname;H;G;numhyps;v;evd)?exname:n.new-do-Elim(exname;H;G;numhyps;n;evd)
Definition: new-evd-proof
new-evd-proof(exname;sequent;evd)
==r let rule,subevd = NewEvdProofStep(exname;sequent;evd)
in let sr ⟵ <sequent, rule>
in let subgoals ⟵ outl(FOLeffect(sr))
in eval n = ||subgoals|| in
if n=0
then <sr, []>
else let s1 ⟵ subgoals[0]
in let evd1 ⟵ subevd[0]
in eval p1 = new-evd-proof(exname;s1;evd1) in
if n=1
then <sr, [p1]>
else let s2 ⟵ subgoals[1]
in let evd2 ⟵ subevd[1]
in eval p2 = new-evd-proof(exname;s2;evd2) in
if n=2
then <sr, [p1; p2]>
else let LL ⟵ tl(tl(upto(n)))
in eval L = map(λi.new-evd-proof(exname;subgoals[i];subevd[i]);LL) in
<sr, [p1; [p2 / L]]>
Definition: new-evd-to-proof
new-evd-to-proof(G;evd) == let p ⟵ ν(ex.new-evd-proof(ex;<[], G>;λM.evd)) in p
Definition: mFO-Kripke-struct
mKripkeStruct ==
K:G:Type × R:G ⟶ G ⟶ ℙ × D:G ⟶ Type × (i:G ⟶ FOStruct(D i)) × let G,R,D,S = K
in (∀i,j:G.
((R i j)
⇒ (((D i) ⊆r (D j))
∧ (∀A:Atom. ∀L:(D i) List.
((S i A L) ⊆r (S j A L))))))
∧ (∀i:G. (R i i))
∧ (∀i,j,k:G. ((R i j) ⇒ (R j k) ⇒ (R i k)))
Lemma: mFO-Kripke-struct_wf
mKripkeStruct ∈ 𝕌'
Definition: K-world
World == fst(fst(K))
Lemma: K-world_wf
∀[K:mKripkeStruct]. (World ∈ Type)
Definition: K-le
i ≤ j == (fst(snd(fst(K)))) i j
Lemma: K-le_wf
∀[K:mKripkeStruct]. ∀[i,j:World]. (i ≤ j ∈ ℙ)
Lemma: K-le_reflexive
∀K:mKripkeStruct. ∀i:World. i ≤ i
Lemma: K-le_transitivity
∀K:mKripkeStruct. ∀i,j,k:World. (i ≤ j ⇒ j ≤ k ⇒ i ≤ k)
Definition: K-dom
Dom(i) == (fst(snd(snd(fst(K))))) i
Lemma: K-dom_wf
∀[K:mKripkeStruct]. ∀[i:World]. (Dom(i) ∈ Type)
Lemma: K-dom_subtype
∀[K:mKripkeStruct]. ∀[i,j:World]. Dom(i) ⊆r Dom(j) supposing i ≤ j
Lemma: K-assignment_subtype
∀[K:mKripkeStruct]. ∀[i,j:World].
∀vs1,vs2:ℤ List. FOAssignment(vs1,Dom(i)) ⊆r FOAssignment(vs2,Dom(j)) supposing vs2 ⊆ vs1 supposing i ≤ j
Definition: K-struct
K-struct(K;i) == (snd(snd(snd(fst(K))))) i
Lemma: K-struct_wf
∀[K:mKripkeStruct]. ∀[i:World]. (K-struct(K;i) ∈ FOStruct(Dom(i)))
Definition: K-sat
i,a |= fmla == Dom(i),K-struct(K;i),a |= mFOL-abstract(fmla)
Lemma: K-sat_wf
∀[K:mKripkeStruct]. ∀[i:World]. ∀[fmla:mFOL()]. ∀[a:FOAssignment(mFOL-freevars(fmla),Dom(i))]. (i,a |= fmla ∈ ℙ)
Definition: K-forces
K-forces(K;fmla) ==
mFOL_ind(fmla;
mFOatomic(R,vars)⇒ λi,a. i,a |= R(vars);
mFOconnect(knd,a,b)⇒ frca,frcb.if knd =a "and" then λi,a. ((frca i a) ∧ (frcb i a))
if knd =a "or" then λi,a. ((frca i a) ∨ (frcb i a))
else λi,a. ∀j:{j:World| i ≤ j} . ((frca j a) ⇒ (frcb j a))
fi ;
mFOquant(isall,z,body)⇒ frcbody.if isall
then λi,a. ∀j:{j:World| i ≤ j} . ∀v:Dom(j). (frcbody j a[z := v])
else λi,a. ∃v:Dom(i). (frcbody i a[z := v])
fi )
Lemma: K_forces_connect_lemma
∀u,v,knd,K:Top.
(K-forces(K;mFOconnect(knd;u;v)) ~ if knd =a "and" then λi,a. ((K-forces(K;u) i a) ∧ (K-forces(K;v) i a))
if knd =a "or" then λi,a. ((K-forces(K;u) i a) ∨ (K-forces(K;v) i a))
else λi,a. ∀j:{j:World| i ≤ j} . ((K-forces(K;u) j a) ⇒ (K-forces(K;v) j a))
fi )
Lemma: K_forces_quant_lemma
∀body,z,isall,K:Top.
(K-forces(K;mFOquant(isall;z;body)) ~ if isall
then λi,a. ∀j:{j:World| i ≤ j} . ∀v:Dom(j). (K-forces(K;body) j a[z := v])
else λi,a. ∃v:Dom(i). (K-forces(K;body) i a[z := v])
fi )
Lemma: K_forces_atomic_lemma
∀vars,R,K:Top. (K-forces(K;R(vars)) ~ λi,a. i,a |= R(vars))
Lemma: K-forces_wf
∀[K:mKripkeStruct]. ∀[fmla:mFOL()]. (K-forces(K;fmla) ∈ i:World ⟶ FOAssignment(mFOL-freevars(fmla),Dom(i)) ⟶ ℙ)
Definition: K-uforces
K-uforces(K;fmla) ==
mFOL_ind(fmla;
mFOatomic(R,vars)⇒ λi,a. i,a |= R(vars);
mFOconnect(knd,a,b)⇒ frca,frcb.if knd =a "and" then λi,a. ((frca i a) ∧ (frcb i a))
if knd =a "or" then λi,a. ((frca i a) ∨ (frcb i a))
else λi,a. ∀[j:World]. (frca j a) ⇒ (frcb j a) supposing i ≤ j
fi ;
mFOquant(isall,z,body)⇒ frcbody.if isall
then λi,a. ∀[j:World]. ∀v:Dom(j). (frcbody j a[z := v]) supposing i ≤ j
else λi,a. ∃v:Dom(i). (frcbody i a[z := v])
fi )
Lemma: K_uforces_connect_lemma
∀v,u,knd,K:Top.
(K-uforces(K;mFOconnect(knd;u;v)) ~ if knd =a "and" then λi,a. ((K-uforces(K;u) i a) ∧ (K-uforces(K;v) i a))
if knd =a "or" then λi,a. ((K-uforces(K;u) i a) ∨ (K-uforces(K;v) i a))
else λi,a. ∀[j:World]. (K-uforces(K;u) j a) ⇒ (K-uforces(K;v) j a) supposing i ≤ j
fi )
Lemma: K_uforces_quant_lemma
∀body,z,isall,K:Top.
(K-uforces(K;mFOquant(isall;z;body)) ~ if isall
then λi,a. ∀[j:World]. ∀v:Dom(j). (K-uforces(K;body) j a[z := v]) supposing i ≤ j
else λi,a. ∃v:Dom(i). (K-uforces(K;body) i a[z := v])
fi )
Lemma: K_uforces_atomic_lemma
∀vars,R,K:Top. (K-uforces(K;R(vars)) ~ λi,a. i,a |= R(vars))
Lemma: K-uforces_wf
∀[K:mKripkeStruct]. ∀[fmla:mFOL()]. (K-uforces(K;fmla) ∈ i:World ⟶ FOAssignment(mFOL-freevars(fmla),Dom(i)) ⟶ ℙ)
Lemma: K-forces-monotone
∀K:mKripkeStruct. ∀fmla:mFOL(). ∀i,j:World.
(i ≤ j ⇒ (∀a:FOAssignment(mFOL-freevars(fmla),Dom(i)). ((K-forces(K;fmla) i a) ⊆r (K-forces(K;fmla) j a))))
Lemma: K-uforces-monotone
∀K:mKripkeStruct. ∀fmla:mFOL(). ∀i,j:World.
(i ≤ j ⇒ (∀a:FOAssignment(mFOL-freevars(fmla),Dom(i)). ((K-uforces(K;fmla) i a) ⊆r (K-uforces(K;fmla) j a))))
Lemma: K-uforces-umonotone
∀K:mKripkeStruct. ∀fmla:mFOL(). ∀i:World.
∀[j:World]
∀a:FOAssignment(mFOL-freevars(fmla),Dom(i)). ((K-uforces(K;fmla) i a) ⊆r (K-uforces(K;fmla) j a)) supposing i ≤ j
Home
Index