Theorem axi12
Axiom of Quantifier Introduction (intuitionistic logic axiom ax-i12). In
classical logic, this is mostly a restatement of axc9 (with one
additional quantifier). But in intuitionistic logic, changing the
negations and implications to disjunctions makes it stronger. Usage of
this theorem is discouraged because it depends on [ax-13]. (Contributed
by Jim Kingdon, 31-Dec-2017.) Avoid [ax-11]. (Revised by Wolf Lammen,
24-Apr-2023.) (New usage is discouraged.)
Conclusion
\( \vdash \forall z \, z = x' \vee (\forall z \, z = y' \vee \forall z \, (x' = y' \rightarrow \forall z \, x' = y')) \)
Proof
l0
nfa1
nfa1
nfor l0 _
l3
19.32 _
\( \vdash \forall z \, (\forall z \, z = x' \vee \forall z \, z = y' \vee (x' = y' \rightarrow \forall z \, x' = y')) \leftrightarrow \forall z \, z = x' \vee \forall z \, z = y' \vee \forall z \, (x' = y' \rightarrow \forall z \, x' = y') \)
axc9
orrd _
l6
orri _
\( \vdash \forall z \, z = x' \vee (\forall z \, z = y' \vee (x' = y' \rightarrow \forall z \, x' = y')) \)
orass
\( \vdash \forall z \, z = x' \vee \forall z \, z = y' \vee (x' = y' \rightarrow \forall z \, x' = y') \leftrightarrow \forall z \, z = x' \vee (\forall z \, z = y' \vee (x' = y' \rightarrow \forall z \, x' = y')) \)
mpbir l6 _
\( \vdash \forall z \, z = x' \vee \forall z \, z = y' \vee (x' = y' \rightarrow \forall z \, x' = y') \)
l9
mpgbi l3 _
\( \vdash \forall z \, z = x' \vee \forall z \, z = y' \vee \forall z \, (x' = y' \rightarrow \forall z \, x' = y') \)
orass
\( \vdash \forall z \, z = x' \vee \forall z \, z = y' \vee \forall z \, (x' = y' \rightarrow \forall z \, x' = y') \leftrightarrow \forall z \, z = x' \vee (\forall z \, z = y' \vee \forall z \, (x' = y' \rightarrow \forall z \, x' = y')) \)
mpbi l9 _