Email Gateway (Aug 19 2022 at 14:00): Email Gateway (Aug 19 2022 at 14:00):From: Gottfried Barrow <igbi@gmx.com>
As to what kind of tableaux it really is, that is questionable.
Please consider this formula:
(A & B) --> C ==> ~A --> D ==> B --> (C | D).
Has it been in your wildest dreams to do the following?
(a) negate the conclusion of that formula,
(b) then expand it into 6 negated chains of conjunctions,
(c) then convert that into a formula that only uses Trueprop, ==>,
False, and bool variables,
(d) and then prove that expression with auto, auto needing none of
this to be done.
It went like this:
(1) I became aware that Larry's blast is used by auto, the word
"tableau" being involved, by necessity implicating that French guy,
Thomas Voeckler.
(2) From looking at a combination of Reeves & Clarke's free logic book,
[1], and the chapter on analytic tableaux in Smullyan, [2], I worked up
some notation to implement the tree of a tableaux for the formula above,
from [1] page 76.
(3) I tried to automate building the binary tree in Isabelle, but
aborted that due to lack of programming skills.
(4) I switched to trying to expand the formula in just the right way, to
get the chains that correspond to the tree.
(5) I stumbled on the right combination of rules needed, at least for
that formula, which is enough for now.
Can we not agree, that ==> is the Isabelle mother-of-all-meta-logic
operators? However, though mothers are very important, even mothers, at
times, need a little help from their children to arrive at the desired
location.
I included the source and attached the THY. Even a true artiste must
continually experiment with notation to find something which meet many,
many needs. Over and over again, initial choices are refined or abandoned.
This will be part of my voluminous work, "The Logic of a True Artiste -
In All Its Majestic Fame and Glory - Alonso Church, You and Haskell
Curry Would be Proud - Donald Knuth, One Word, LaTeX - Mike Gordon, You
Are Absent from This Mailing List, Three Letters, HOL - Robin Milner,
It's Enough to Say Your Name."
Regards,
GB
[1] Logic for Computer Science, http://www.cs.waikato.ac.nz/~stever/LCS.html
[2] First-order logic,
http://www.amazon.com/First-Order-Logic-Dover-Books-Mathematics/dp/0486683702
(******************)
theory i140309aa__semantab
imports Complex_Main ("../../iHelp/i") (*"../../IsaN/work/IsaN" *)
begin
(*( \<turnstile> ): Turnstile to shorten the notation for
meta-implication.*)
no_notation ==> (infixr "\<turnstile>" 4)
abbreviation mimp_turn :: "prop \<Rightarrow> prop \<Rightarrow> prop" where
"mimp_turn P Q == (PROP P \<Longrightarrow> PROP Q)"
notation mimp_turn (infixr "\<turnstile>" 4)
(*( \<cedilla> ): Cedilla, to act as a comma, for formulas such as
P\<cedilla> Q \<turnstile> R.*)
notation (input) ==> (infixr "\<cedilla>" 4)
(*( \<bottom> ): False, to shorten the notation. The output is bold for
visibility.*)
notation (input) False ("\<bottom>")
notation (output) False ("\<^bold>\<bottom>")
(( \<cdot>~\<cdot> ): notP, PROP not.)
abbreviation notP :: "prop \<Rightarrow> prop" where
"notP P == (PROP P \<Longrightarrow> False)"
notation notP ("\<cdot>~\<cdot>'(_')") (* \<cdot>~\<cdot> *)
(*( \<or>\<^sub>p ): orP, PROP disjunction.*)
(PROP or: orP)
abbreviation orP :: "prop \<Rightarrow> prop \<Rightarrow> prop" where
"orP P Q == ((PROP P \<Longrightarrow> False) \<Longrightarrow> PROP Q)"
notation
orP (infixr "(\<or>\<^sub>p)" 4)
(*( \<and>\<^sub>p ): andP, PROP conjunction.*)
abbreviation andP :: "prop \<Rightarrow> prop \<Rightarrow> prop" where
"andP P Q == ((PROP P \<Longrightarrow> PROP Q \<Longrightarrow>
False) \<Longrightarrow> False)"
notation
andP (infixr "(\<and>\<^sub>p)" 4)
(*( \<and>\<^sub>4 ): and4, bool conjunction with the same priority as
andP. For conversions
from bool to PROP, to ensure that the same parenthesizing applies.*)
abbreviation (input) and4 :: "bool \<Rightarrow> bool \<Rightarrow>
bool" where
"and4 P Q == (P \<and> Q)"
notation
and4 (infixr "(\<and>\<^sub>4)" 4)
(*******)
(* LOGIC RULES *****)
(*******)
lemma mimp2in_to_3and_mimps_False:
"P\<cedilla> Q \<turnstile> R == P \<and>\<^sub>4 Q \<and>\<^sub>4
\<not>R \<turnstile> False"
by(rule equal_intr_rule, auto)
lemma or6_mimps_False_to_6andP_of_notPs:
"P\<^sub>1 \<or> P\<^sub>2 \<or> P\<^sub>3 \<or> P\<^sub>4 \<or>
P\<^sub>5 \<or> P\<^sub>6 \<turnstile> False
== \<cdot>~\<cdot>(P\<^sub>1) \<and>\<^sub>p
\<cdot>~\<cdot>(P\<^sub>2) \<and>\<^sub>p \<cdot>~\<cdot>(P\<^sub>3)
\<and>\<^sub>p \<cdot>~\<cdot>(P\<^sub>4) \<and>\<^sub>p
\<cdot>~\<cdot>(P\<^sub>5) \<and>\<^sub>p \<cdot>~\<cdot>(P\<^sub>6)"
by(rule equal_intr_rule, auto)
lemma and_eq_andP:
"Trueprop(P \<and> Q) == P \<and>\<^sub>p Q"
by(rule equal_intr_rule, auto)
lemma not_eq_notP:
"Trueprop(\<not>P) == \<cdot>~\<cdot>(P)"
by(rule equal_intr_rule, auto)
lemmas semantab_bool_expansion =
simp_thms(1)
imp_conv_disj
de_Morgan_conj
de_Morgan_disj
conj_comms
conj_disj_distribL
disj_assoc
lemmas semantab_bool_to_prop =
and_eq_andP
not_eq_notP
(******)
(* THEOREM ****)
(******)
notation Trueprop ("_\<Colon>\<^sub>T" [1000] 1000)
declare[[show_sorts=false, show_types=false, show_brackets=true]]
lemma
"(A \<and> B) \<longrightarrow> C\<cedilla> \<not>A \<longrightarrow>
D \<turnstile> B \<longrightarrow> (C \<or> D)"
unfolding mimp2in_to_3and_mimps_False
unfolding semantab_bool_expansion
unfolding or6_mimps_False_to_6andP_of_notPs
unfolding semantab_bool_to_prop
by(auto)
lemma
"(A \<and> B) \<longrightarrow> C\<cedilla> \<not>A \<longrightarrow>
D \<turnstile> B \<longrightarrow> (C \<or> D)"
(*|Negate the conclusion and convert it to a 3-bool-and that mimps False.
The notation for (P \<turnstile> False) is \<cdot>~\<cdot>(P).
Because of requirements due to Trueprop
and other low priorities, notP needs to be in parentheses.|*)
unfolding mimp2in_to_3and_mimps_False
(*|Expand the bool formulas. The result will be a 6-bool-or that is
nested to
the left, and that mimps False.|*)
unfolding
simp_thms(1)
imp_conv_disj
de_Morgan_conj
de_Morgan_disj
conj_comms
conj_disj_distribL
(|Nest the 6-bool-or to the right.|)
unfolding disj_assoc
(|Convert the 6-bool-or to 6 chains of andP-ands that each mimp False.|)
unfolding or6_mimps_False_to_6andP_of_notPs
(|Convert the bool-nots and bool-ands to notP-nots and andP-ands.|)
unfolding and_eq_andP
unfolding not_eq_notP
(*Now, there is no use of HOL in the formula except for the use of Trueprop
and False. This can be seen by the fact that all of A, B, C, and D
are being
coerced by Trueprop. To turn the Trueprop printing off, change
notation above
to no_notation.*)
using[[show_sorts=false, show_types=false, show_brackets=false]]
(*The definition is shown as follows, from HOL.thy:
defs
True_def: "True == ((%x::bool. x) = (%x. x))"
All_def: "All(P) == (P = (%x. True))"
Ex_def: "Ex(P) == !Q. (!x. P x --> Q) --> Q"
False_def: "False == (!P. P)"
It's defined using only All and True, however, obviously, it's
totally tied
into the logic of HOL. But then, that's what makes auto work by magic
when
used above, and below.
Of course, auto doesn't need any of this to be done for this theorem,
but
it could be that auto will be grateful someday. On the other hand,
it's more
likely that auto is an emotionless automaton, who doesn't care
whether I live
or die. In that case, it will be me who is grateful someday.*)
by(auto)
(******************)
end
i140309aa__semantab.thy
Last updated: Apr 20 2024 at 12:26 UTC