Discussion:
What are Semantic Atoms ???
(too old to reply)
Pete Olcott
2017-06-09 13:04:12 UTC
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
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
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
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
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
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
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) *
António Marques
2018-02-24 05:16:13 UTC
Permalink
Raw Message
Post by Pete Olcott
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.
Come again? Where’s the... logic... in that?
Pete Olcott
2018-02-24 05:42:24 UTC
Permalink
Raw Message
Post by António Marques
Post by Pete Olcott
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.
Come again? Where’s the... logic... in that?
I want to always have three copies of every post archived.
--
*∀L ∈ Formal_Systems
∀X
True(L, X) ↔ ∃Γ ⊆ Axioms(L) Provable(Γ, X) *
António Marques
2018-02-24 15:31:44 UTC
Permalink
Raw Message
Post by Pete Olcott
Post by António Marques
Post by Pete Olcott
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.
Come again? Where’s the... logic... in that?
I want to always have three copies of every post archived.
So you’re one of those who think USENET is their personal notepad?
Pete Olcott
2018-02-24 16:00:20 UTC
Permalink
Raw Message
Post by António Marques
Post by Pete Olcott
Post by António Marques
Post by Pete Olcott
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.
Come again? Where’s the... logic... in that?
I want to always have three copies of every post archived.
So you’re one of those who think USENET is their personal notepad?
As will be shown my work changes the foundation of mathematics
and computer science, thus must be well-documented.

The reason that I am doing this work is to establish the foundation
for the formalization of natural language.

The reason for doing that is to create a fully functional human
mind from non-living material (silicon and software).
--
*∀L ∈ Formal_Systems
∀X
True(L, X) ↔ ∃Γ ⊆ Axioms(L) Provable(Γ, X) *
Pete Olcott
2018-02-26 18:21:52 UTC
Permalink
Raw Message
[ Followup-To: poster ]
What's extraordinary is that you can't see how this makes you look. Do
you have any friends or family whose opinion about social matters you
trust? If so, show them this post and take what they say about it
seriously. They don't have to know anything about mathematics, just
about how the world of academic ideas works. They might suggest you
seek help. I certainly would.
The foundation of mathematics gets changed by published papers, not by
doodles in some crank-infested corner of the internet. Even if your
ideas were new and sound, you would risk being mistaken for a crank
simply by not publishing in a proper journal.
Thank you for pointing out what Pete Olcott's problem is.
It is entirely irrelevant whether mathematical methods have ever had a
place in linguistics, and, if not, whether one can conclude that they will
never have. It is only relevant whether Pete Olcott can present results
that are mathematically sound, and only if so, whether he can explain in
which way they could be interesting for linguistics. As far as I have seen
in the past years, he has failed in both respects.
Here are mathematically sound results of applying formal logic to
http://www.cyc.com/documentation/ontologists-handbook/writing-efficient-cycl/cycl-representation-choices/
No real mathematician would consider what ontologists do as
mathematics. What cycorp does is not even applied
mathematics. Merely using symbols does not make something
mathematics.
I observe that Cycorp announced that their AI engine was now
complete in its generic form. Now the experiment as to what
extent it works begins.
Heh you never answered my rebuttal about how the notion of Truth is defined in mathematics.

You claimed that it is specified differently than what I am saying.

I am saying that it is mostly not specified at all.

Here is my definition of Truth for all formal and natural languages:
http://liarparadox.org/index.php/2018/02/17/the-ultimate-foundation-of-a-priori-truth/

Here is what I found that Math says about Truth:
https://en.wikipedia.org/wiki/Philosophy_of_mathematics
It is a profound puzzle that on the one hand mathematical truths seem to have a compelling inevitability, but on the other hand the source of their "truthfulness" remains elusive.
--
*∀L ∈ Formal_Systems
∀X
True(L, X) ↔ ∃Γ ⊆ Axioms(L) Provable(Γ, X) *
Loading...