Email Gateway (Feb 01 2025 at 09:15): Email Gateway (Feb 01 2025 at 09:15):From: Oleksandr Gavenko <gavenkoa@gmail.com>
I'm an enthusiast of math logic so what I'm doing with Isabelle is not for
something beneficial IRL, skip the mail if you value your time ))
In David Hilbert's book
https://en.wikipedia.org/wiki/Grundlagen_der_Mathematik there is a
methodology to prove axiom independence via a model.
A trivial informal example of independence proof: if we assign usual truth
table for T / F for implication and define _ & _ = F (for conjunction) we
get following as tautologies:
(A & B)⟶A -- (F⟶_) ≡ T
(A & B)⟶B
Also MP rule keeps tautology status.
But following statement (&-introduction) is not a tautology:
A⟶B⟶(A & B) -- (T⟶F) ≡ F, so (T⟶(T⟶F)) ≡ F
So this axiom is independent from any implication axioms and &-elimination
axioms.
I asked the question earlier here:
I don't understand how to define truth tables and prove statements about
operations, defined by truth tables.
My naive HOL code is:
theory ax_ind
imports Main
begin
datatype truth = T | F
lemma truth_dom: "a = T ∨ a = F"
by (cases a, clarify+)
fun impl :: "truth⇒truth⇒truth" where
"impl F F = T" |
"impl F T = T" |
"impl T F = F" |
"impl T T = T"
notation impl (infixr ‹→› 65)
value "(T→F)"
fun conja :: "truth⇒truth⇒truth" where
"conja F F = F" |
"conja F T = F" |
"conja T F = F" |
"conja T T = F"
notation conja (infixr ‹&› 60)
value "(T → F) → (F & T)"
(* example of tautology proof *)
lemma "((P::truth) → P) = T"
by(cases P, auto)
(* example of inference rule keeping tautology *)
lemma
fixes P::truth and Q::truth
assumes "P = T" and "(P→Q) = T"
shows "Q = T"
proof (rule ccontr)
assume "Q ≠ T"
then have "Q = F" using truth_dom by (auto)
then have "P→Q = F" using assms(1) by (auto)
then show False using assms(2) by auto
qed
(* example of non-tautology *)
lemma "∃ P Q. P → Q → (P & Q) = F"
proof -
have "(T → T → (T & T)) = F" by auto
then show ?thesis by auto+
qed
Above code is a rudimental attempt, things I don't like and hope veterans
could reference to examples or suggest improvement:
I made "fun" working only by providing all combinations of truth values.
In Hilbert's original work he used schematic rules, which shortens truth
tables and even denote "ideas". If I start encoding 3 or 4 values truth
tables patterns becomes handy:
shorter definitions
My attempts to define "a -> a = T" resulted in an error "Nonlinear patterns
not allowed in sequential mode", probably I need to read functions.pdf.
??? What is the way to define a truth table for operators via helpful
patterns?
I have a wild guess that the above code is already like "embedded logic".
It might lack some syntax sugar, like operator ⊨, how can I define it?
Naive pseudocode is:
definition ⊨::"truth => bool"
where "⊨ expr ⟷ (expr = T) ∨ (expr = α) ∨ (expr = β)
IDK how to capture variable number of free variables in "expr". Because an
expression is a tautology when every truth table substitution leads to a
selected truth value set. Like:
⊨A→B→A
actually means:
∀ A B. A→B→A ∈{T, α, β}
And independence of an axiom is a statement that exist values for variables
of "expr" that results to non-true truth value:
∃ A B. A→B→(A&B) ∉{T, α, β}
??? With my knowledge of Isabelle I cannot express a statement about *all
variables, participating in formula* and quantify them as All or Ex.
Seems latter ⊭ (non-tautology) could be defined as negation of ⊨.
It looks like some evaluator (or "image" creator) should be defined over
expressions. Some values will denote "true", and theorems might look like
in pseudocode:
fact: true_val(model) ∈{T, α, β}
fact: img_of (expr in model) ⊆ true_val(model) (* image of expr over all
possible substitution of variables in expr *)
lemma "model ⊨(A → A)"
??? What way could the model be externalized or abstracted and different
instances could be referenced for a given expression?
Hilbert used 3-4 valued truth tables in his work. I believe it is
manageable for Isablelle.
Email Gateway (Feb 01 2025 at 09:16):From: Oleksandr Gavenko <gavenkoa@gmail.com>
I'm an enthusiast of math logic so what I'm doing with Isabelle is not
for something beneficial IRL, value your time ))
In David Hilbert's book
https://en.wikipedia.org/wiki/Grundlagen_der_Mathematik there is a
methodology to prove axiom independence via a model.
A trivial informal example of independence proof: if we assign usual
truth table for T / F for implication and define _ & _ = F (for
conjunction) we get following as tautologies:
(A & B)⟶A -- (F⟶_) ≡ T
(A & B)⟶B
Also MP rule keeps tautology status.
But following statement (&-introduction) is not a tautology:
A⟶B⟶(A & B) -- (T⟶F) ≡ F, so (T⟶(T⟶F)) ≡ F
So this axiom is independent from any implication axioms and
&-elimination axioms.
I asked the question earlier here:
I don't understand how to define truth tables and prove statements
about operations, defined by truth tables.
My naive HOL code is:
theory ax_ind
imports Main
begin
datatype truth = T | F
lemma truth_dom: "a = T ∨ a = F"
by (cases a, clarify+)
fun impl :: "truth⇒truth⇒truth" where
"impl F F = T" |
"impl F T = T" |
"impl T F = F" |
"impl T T = T"
notation impl (infixr ‹→› 65)
value "(T→F)"
fun conja :: "truth⇒truth⇒truth" where
"conja F F = F" |
"conja F T = F" |
"conja T F = F" |
"conja T T = F"
notation conja (infixr ‹&› 60)
value "(T → F) → (F & T)"
(* example of tautology proof *)
lemma "((P::truth) → P) = T"
by(cases P, auto)
(* example of inference rule keeping tautology *)
lemma
fixes P::truth and Q::truth
assumes "P = T" and "(P→Q) = T"
shows "Q = T"
proof (rule ccontr)
assume "Q ≠ T"
then have "Q = F" using truth_dom by (auto)
then have "P→Q = F" using assms(1) by (auto)
then show False using assms(2) by auto
qed
(* example of non-tautology *)
lemma "∃ P Q. P → Q → (P & Q) = F"
proof -
have "(T → T → (T & T)) = F" by auto
then show ?thesis by auto+
qed
Above code is a rudimental attempt, things I don't like and hope
veterans could reference to examples or suggest improvement:
I made "fun" working only by providing all combinations of truth
values. In Hilbert's original work he used schematic rules, which
shortens truth tables and even denote "ideas". If I start encoding 3
or 4 values truth tables patterns becomes handy:
shorter definitions
My attempts to define "a -> a = T" resulted in an error "Nonlinear
patterns not allowed in sequential mode", probably I need to read
functions.pdf.
??? What is the way to define a truth table for operators via helpful patterns?
I have a wild guess that the above code is already like "embedded logic".
It might lack some syntax sugar, like operator ⊨, how can I define it?
Naive pseudocode is:
definition ⊨::"truth => bool"
where "⊨ expr ⟷ (expr = T) ∨ (expr = α) ∨ (expr = β) (* values, that
are considered "true" *)
IDK how to capture variable number of free variables in "expr".
Because an expression is a tautology when every truth table
substitution leads to a selected truth value set. Like:
⊨A→B→A
actually means:
∀ A B. A→B→A ∈{T, α, β}
And independence of an axiom is a statement that exist values for
variables of "expr" that results to non-true truth value:
∃ A B. A→B→(A&B) ∉{T, α, β}
??? With my knowledge of Isabelle I cannot express a statement about
all variables, participating in formula and quantify them as All or
Ex.
Seems latter ⊭ (non-tautology) could be defined as negation of ⊨.
It looks like some evaluator (or "image" creator) should be defined
over expressions. Some values will denote "true", and theorems might
look like in pseudocode:
fact: true_val(model) = {T, α, β}
fact: img_of (expr in model) ⊆ true_val(model) (* image of expr over
all possible substitution of variables in expr *)
lemma "model ⊨(A → A)"
??? What way could the model be externalized or abstracted and
different instances of model could be referenced for a given
expression?
Hilbert used 3-4 valued truth tables in his work. I believe it is
manageable for Isablelle.
PS I've sent an email to the list isabelle-users@cl.cam.ac.uk
initially, probably that is a legacy one.
PPS I searched for "⊨", "sound", "complete" in Isablelle's src/ &
AFP's thys/, the latter has many examples that might be relevant for
the goal. Variables are defined as "nat" and so on (from Cook_Levin
folder of AFP):
datatype literal = Neg nat | Pos nat
type_synonym clause = "literal list"
type_synonym formula = "clause list"
type_synonym assignment = "nat ⇒ bool"
abbreviation satisfies_literal :: "assignment ⇒ literal ⇒ bool" where
"satisfies_literal α x ≡ case x of Neg n ⇒ ¬ α n | Pos n ⇒ α n"
definition satisfies_clause :: "assignment ⇒ clause ⇒ bool" where
"satisfies_clause α c ≡ ∃x∈set c. satisfies_literal α x"
definition satisfies :: "assignment ⇒ formula ⇒ bool" (infix ‹⊨› 60) where
"α ⊨ φ ≡ ∀c∈set φ. satisfies_clause α c"
Above is specialized logic, other theories define formulas as
recursive data structures. I think I lose human readable axiom
representation because of "constructor" syntax of types. Dealing with
"nat" or formula "trees" is not fun ((
That gives me ideas but I'm inexperienced with Isabelle enough to come
up with some clever abstraction so I can reason about validity of
expression under a given model.
Last updated: Mar 09 2025 at 12:28 UTC