Discussion:
What are Semantic Atoms ???
Add Reply
Pete Olcott
2017-06-09 13:04:12 UTC
Reply
Permalink
Raw Message
I am working on the YACC BNF syntax of Minimal Type Theory.
It will end up being a subset of "C" for functions and FOPL syntax (not semantics) that has been strongly typed using the proper classes of NBG axiomatic set theory.
This I will have to see before I believe.
I have the first draft almost complete, I have one YACC shift-reduce conflict to resolve.
The FOPL portion is identical to FOPL, except that it is a strongly typed language, requiring that everything has its type explicitly specified.
--
(Γ ⊨ _FS A) ≡ (Γ ⊢ _FS A)
Pete Olcott
2017-06-09 13:14:59 UTC
Reply
Permalink
Raw Message
http://liarparadox.org/Provability_with_Minimal_Type_Theory.pdf
That it is a key aspect of such a system is directly demonstrated in that this system closes the semantic gaps of the original (1931) Incompleteness Theorem showing the fundamental error of this proof.
I am currently in the process of transforming this design into a fully operational knowledge ontology that can concretely demonstrate semantic logical entailment on the basis of meaning postulate axioms.
I could guess at your intentions - but why bother. Present
a theory of MTT and we can comment.
http://www.cyc.com/documentation/ontologists-handbook/
It is the same sort of thing as CycL, except simpler and the key distinction is that the design of my system is based on sub atomic semantic compositionality where everything (semantics of all operators, rules of inference) besides machine memory addressing is explicitly specified as an axiom.

{Iteration:while, Selection:if-else, Sequence}
Types:
Character // UTF-32
String // of Characters
Index // __int64 subscript of String
Number // String of digits
Unit of composition: Function
--
(Γ ⊨ _FS A) ≡ (Γ ⊢ _FS A)
Pete Olcott
2017-06-16 21:59:52 UTC
Reply
Permalink
Raw Message
No that is the whole point. They never tell me where I am wrong they only are able to say that they really, really believe that I must be wrong, yet can never ever point to where.
James Burns in sci.math understands modern mathematical logic and tells you
where you go wrong. He also said in the recent Goedel thread
You show the signs of someone who is using technical terms without
understanding, as technobabble or bafflegab.
It may appear to the outside observer that my command of the various divergent terminology from the sub-fields of logic is incorrect because it is not always perfectly consistent with the conventional meaning in each of these diverse sub-fields.

I am not approaching these things from the frame-of-reference of conventional terminology or notational conventions because both are insufficiently expressive to convey my new insights.

I am approaching these things as pure conceptions beyond words. The conceptions themselves are my target the words are an after-thought.

This all would be totally useless if I was not also deriving a precise mathematical specification for these new insights. I have the YACC BNF grammar for Minimal Type Theory almost complete.

As I have been saying all along (even in the nearly final design) it has syntax (NOT SEMANTICS) that is mostly an augmentation to FOPL syntax (NOT SEMANTICS) to ensure that every variable is of a specific type.

The only other difference from FOPL syntax (NOT SEMANTICS) is that I am using Jim's suggested "@" <assign_alias> operator so that an expression can refer to itself:

// This expression is neither provable nor refutable in every formal system
// because is has pathological self-reference:
G @ ∀L ∈ Formal_Systems, ~∃Γ ⊂ L (Γ ⊢ G)

"@" means the LHS is assigned as an alias for the RHS.
There is no referencing / dereferencing needed, G is one and the same thing as the expression that refers to G. G is not referring to its name, G is referring to itself.

Above is Copyright 2017 Pete Olcott
Peter Percival
2017-06-17 13:43:18 UTC
Reply
Permalink
Raw Message
Post by Pete Olcott
[...]
The FOPL portion is identical to FOPL, except that it is a strongly
typed language, requiring that everything has its type explicitly
specified.
It may be that what you want is a many-sorted first order theory. But
note that if S1 and S2 are sorts you may have, e.g.,

(forall x of sort S1)(exists y of sort S2)(...)

you may not have

(forall x of sort S1)(exists y subset of sort S2)(...)

because that is no longer first-order.
--
Do, as a concession to my poor wits, Lord Darlington, just explain
to me what you really mean.
I think I had better not, Duchess. Nowadays to be intelligible is
to be found out. -- Oscar Wilde, Lady Windermere's Fan
Pete Olcott
2018-02-23 13:54:03 UTC
Reply
Permalink
Raw Message
Peter Olcott or Pete Olcott returned, and already starts multiplying his
threads, instead of developing an idea in a single thread, so I revive
this thread here, as he goes on reducing natural logic to mathematical
logic, and driving life out of language.
Peter Olcott is again multiplying his threads, decided to take over also
sci.lang in the name of his phantasm of the absolute and complete and total
truth, never saying anything understandable let alone useful about language,
providing ever more final and finaller and more ultamterer versions of his
alleged proofs that Goedel and Turing were wrong, not understanding their
work, claiming that the truth has always been his first priority, yet
dismissing some of the finest pieces of truth humankind achieved, the proven
theorems of Goedel and Turing, by mere word magic and lines that look as if
they were logical formulae but are not, which is why he never can finish
his papers, only shove around the bug.
You're not the person most suited to write this,
but I agree that Peter Olcott's outpours of delirium do not belong here.
A.
What is Linguistics about if it is not about the notion of Truth within language? That none of you guys have enough math background to understand that I just refuted Tarski Undefinability is no indication what-so-ever that my posts pertaining to the same do not belong in sci.lang.

My Halting Problem proofs don't belong in a sci.lang forum and I only cross post some of them because there is a guy here that is also in the comp.theory forum.

To update the details of this post:

Semantic subatomic compositionality is the constituent parts of a semantic atom. A semantic atom is one whole relation/predicate from predicate logic.

Semantic atoms are connected to their constituent parts as the directed paths from nodes in a directed acyclic graph. Each node and each directed path of this Relation is a unit of subatomic semantic compositionality.

By forming these relations this way one can see for the first time how the constituent parts of a relation relate to each other in two dimensional space.

Higher Order Logic expressions are translated into directed acyclic graphs in strict left-to-right becomes top to bottom order. Identifiers are not duplicated.

The first reference to an identifier in a HOL expression is the only instance that is copied to the directed acyclic graph. All other references to this identifier have directed paths formed to this single reference.

By doing this we can see exactly how and why the Liar Paradox is semantically ungrounded as Kripke pointed out in his famous paper: [Outline of a Theory of Truth] Saul Kripke (1975)
http://web.dfc.unibo.it/paolo.leonardi/materiali/cs/Kripke.pdf

This is the key aspect of Minimal Type Theory that allows pathological self-reference(Olcott 2004) to be detected and rejected as semantically incorrect.

Prior to minimal type theory there were many expressions of language that were thought to be paradoxical rather than simply incorrect.

"This sentence is not true"
LP ≡ ~True(LP) // HOL with self-reference semantics

"This sentence is not provable"
G ≡ ~∃Γ Provable(Γ, G) // HOL with self-reference semantics

Tarski's undefinability theorem Wikipedia
"The undefinability theorem shows that this encoding cannot be done
for semantic concepts such as truth. It shows that no sufficiently
rich interpreted language can represent its own semantics."

The following link shows exactly how to define a Truth predicate in each formal or natural language, thus directly refuting Tarski by doing what he concluded was impossible.
http://liarparadox.org/index.php/2018/02/17/the-ultimate-foundation-of-a-priori-truth/

When we plug the Liar Paradox or the simplified Incompleteness Theorem into the above Truth formula we see that the David Hilbert style formalist syntactic logical inference chain (formal proof) never reaches either True or False.

Unlike historical misconceptions the 1931 GIT is not True and improvable, it is simply incorrect because it is neither True nor False.

Copyright 2016, 2017, 2018 Pete Olcott
--
*∀L ∈ Formal_Systems
∀X
True(L, X) ↔ ∃Γ ⊆ Axioms(L) Provable(Γ, X) *
c***@optonline.net
2018-02-23 19:36:39 UTC
Reply
Permalink
Raw Message
Why don't you post so others can easily read ?!

You know, like the original post .
Pete Olcott
2018-02-23 19:49:47 UTC
Reply
Permalink
Raw Message
Post by c***@optonline.net
Why don't you post so others can easily read ?!
You know, like the original post .
This stuff has been evolving over time. Here are some key articles:

https://www.researchgate.net/publication/315367846_Minimal_Type_Theory_MTT

https://www.researchgate.net/publication/317953772_Provability_with_Minimal_Type_Theory

https://www.researchgate.net/publication/323268530_Defining_a_Decidability_Decider
--
*∀L ∈ Formal_Systems
∀X
True(L, X) ↔ ∃Γ ⊆ Axioms(L) Provable(Γ, X) *
Loading...