There are millions of lines that support those functions.Logik wrote: ↑Thu Apr 25, 2019 7:30 pmAlso. I can't parse any of that. It's in some made up language that I don't care to learn.PeteOlcott wrote: ↑Thu Apr 25, 2019 7:13 pm Axiom(0) Stipulates** this definition of Axiom:
Expressions of language defined to have the semantic value of Boolean True.
Provides the symbolic logic equivalent of true premises.
Stipulating** this specification of True and False: (TRUE ↔ ⊤ ∧ FALSE ↔ ⊥)
Axiom(1) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F, x) ↔ (F ⊢ x))
Axiom(2) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (False(F, x) ↔ (F ⊢ ¬x))
Thus stipulating** that consequences are provable from axioms.
Stipulating** that formal systems are Boolean:
Axiom(3) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F,x) ∨ False(F,x))
Screens out semantically unsound sentences as not belonging to the formal system.
Write it in C++.
I am most interested in these functions:
True()
False()
Closed_WFF()
↔()
∈()
The exact same thing can be explained in terms of a Prolog query.
A Prolog query returns: "Yes" for True
and "Yes" for the negation of the query for False.
Everything else is unsound.
Prolog would say: "No"
there are statements of the language of F which can neither be proved nor disproved in F. (Raatikainen 2018)
Thus refuting the 1931 Incompleteness Theorem.
Prolog would say: "No"
(3) x ∉ Pr if and only if x ∈ Tr
Because in Prolog ONLY Provable means True.
Thus refuting the Tarski Undefinability Theorem.