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
Loading...