polcott

@confusedcius Yes you are correct I had a syntax error:
∃L ∈ Formal_Systems, ∃x ∈ L (True(L, x) ≡ (L ⊢ x))
∃L ∈ Formal_Systems, ∃x ∈ L (False(L, x) ≡ (L ⊢ ~x))
∃L ∈ Formal_Systems, ∃x ∈ L (Truth_Bearer(L, x) ≡ (True(L, x) ∨ False(L, x)) )

https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
I created Minimal Type Theory so that I could concisely encode actual self-reference.
In all the literature it is conventional to encode self-reference incorrectly.
LP := ~True(LP)

@confusedcius >>>prolog rules and back-chained inference is quite different from inference in natural language, so it's not obvious that it would translate well.<<< Not at all humans do the exact same thing. Humans may be able to skip a few steps by having the results of the intermediate steps memorized.

>>>prolog assumes any fact not stated is false<<< Not really instead (negation as failure) assumes that any Fact not stated is untrue.

>>>horn clauses is restrictive of the structure of facts one can state<<< I am not referring to that aspect of Prolog. The key aspect of Prolog that I am …

@confusedcius Every expression of language that is {true on the basis of its meaning} is untrue unless it has a connection to its truth-maker. I am using proof theory, not model theory, thus all meaning is formalized and True(L,x) is a relation between finite strings.

A contradiction only actually means FALSE and nothing more or less than that. Marilyn Vos Savant (World's highest IQ) seems to be correct that (paraphrase) education systems abolish all independent thought and replace it with conformity.