Liste des Groupes | Revenir à s logic |
Am Fri, 14 Mar 2025 22:54:51 -0500 schrieb olcott:That is like me saying that you are to stupid toOn 3/14/2025 8:57 PM, Richard Damon wrote:So is the Liar sentence false or not?On 3/14/25 3:01 PM, olcott wrote:On 3/14/2025 1:42 PM, Richard Damon wrote:On 3/14/25 10:27 AM, olcott wrote:On 3/13/2025 6:08 AM, Mikko wrote:On 2025-03-11 23:26:28 +0000, olcott said:On 3/11/2025 6:15 AM, Mikko wrote:Does not define any theory.On 2025-03-10 15:36:28 +0000, olcott said:>
>I created Minimal Type Theory such that self-reference can beHave you pbulished that "Minimal Type Theory" or put it to a web
expressed concisely and correctly.
page?
Without a pointer to it there is no point to mention it. Of
course one can create a language that can express a self
reference but why would one?
https://www.researchgate.net/
publication/315367846_Minimal_Type_Theory_MTT
>https://www.researchgate.net/The article 315367846_Minimal_Type_Theory_MTT says that "Types must
publication/331859461_Minimal_Type_Theory_YACC_BNF
be expressly stated in Minimal Type Theory" but the syntax allows
untyped quantification.
>https://www.researchgate.net/This article uses @ as definition article but a comment in the
publication/317953772_Provability_with_Minimal_Type_Theory
syntax says that := is used.
None of the articles defines what is a valid proof in Minimal Type
Theory.
>We need such a language so that we don't stupidly fail to
understands how this can convert expressions of language into
non-truth-bearers having no truth value.
Until we do this we get confused into believing that such
expressions are in any way undecidable.
>LP := ~True(LP) obtains its entire semantics from the expression.>>Apparently this cannot be expressed concisely and correctly inA self reference cannot be expressed in an uninterpreted formal
any formal logic system.
language.
Sometimes some symbols and expressions are interpreted to
represent themselves or other symbols or expressions. For
example, the symbol 0 of arthmetic can be interpreted to mean the
symbol 0 and the term S0 the sqence of symbols S and 0.
LP := ~True(LP)
has all of its semantics encoded in its syntax, thus no
interpretation required.
Without decoding no semantics can be extracted from the syntax.
>
But none of your arguments have talked about an expression that
derives itself from that expressionBecause of the cycle in the directed graph of its evaluationBut the p that can be developed as a statement in the languaged,
sequence LP cannot derive its semantic meaning from anything else:
~True(~True(~True(~True(~True(~True(...))))))
based on the idea in the metalanguge that must be true if and only if
it is false, doesn't.Normally expressions derive their semantics from a knowledgeRight, like Godel's expression G specifically derives its semantics
ontology inheritance hierarchy.
https://en.wikipedia.org/wiki/Ontology_(information_science)
from the natured of the system F and the mathematics the system F
creates. And, in the meta we can construct a mathematical statement
in F, whose truth is the direct opposite of its provability, and thus
must be True and Unprovable, as it can't be False but Provably True.*Need*? You can always construct a metalanguage.In my type theory based system there is no need for any separateof the set of general knowledge of the world encoded as RudolfWHich is irrelevent here, as Formal systems don't have that problem.
Carnap meaning postulates using something like Montague Grammar.
Each unique sense meaning has its own GUID.
Your problem
language and meta-language.
Discard all inferior systems.Rudolf Carnap meaning postulates are arranged in an inheritancebut the existing systens aren't built on your "Type Theory" so you need
hierarchy where each unique sense meaning is assigned its own GUID.
The language is something like Montague Grammar.
LP := ~True(LP) is rejected as semantically incorrect.
to show that it works in THOSE systems to use it,Wonderful. So not always.I guess you are just admitting that you don't understand what you areWe axiomatize all the basic facts of the world (facts that cannot be
talking about, and your "logic" assumes you can just make up crap and
call it true,
derived on the basis of other facts).
Then we plug everything else into an inheritance hierarchy knowledge
ontology.
Anything that cannot be derived by applying Truth preserving operations
to these basic facts is either untrue or unknown.
This gives us a True() predicate that always works except for unknowns.
It certainty does not get totally confused by self-contradictoryYeah, it can't decide their truth value.
expressions. These simply cannot be derived by applying truth preserving
operations to basic facts.
Les messages affichés proviennent d'usenet.