| Liste des Groupes | Revenir à c theory |
On 6/29/2026 9:31 PM, André G. Isaak wrote:No, they are not. No author writing in the framework of proof-theoretic semantics has ever offered those examples or comparable examples or made any claims about 'rejecting expressions as proof theoretic semantically incoherent'. And there's nothing incoherent about the statement 'no number is equal to its successor' which is the example under discussion.On 2026-06-29 20:17, olcott wrote:Those are specific concrete examples of howOn 6/29/2026 8:54 PM, André G. Isaak wrote:>On 2026-06-29 19:19, olcott wrote:% This sentence is not true.On 6/29/2026 8:01 PM, André G. Isaak wrote:>On 2026-06-29 18:37, olcott wrote:>On 6/29/2026 6:45 PM, André G. Isaak wrote:>On 2026-06-29 17:36, olcott wrote:>>It does seem that they do agree that no proof>
of G can possibly exist in PA does means that
G has no semantic meaning in PA.
I've not seen anyone operating in PTS who says anything remotely like that. They do not agree with this; rather, you are projecting your own peculiar views onto their theory.
>
André
>
Because they beat around the bush about that using
terminology that varies across every author.
It's not that they are beating around the bush; it's that they aren't actually saying what you want them to say. Face it, you really don't understand the PTS literature as it is above your head.
>
André
>
PTS is the way that meaning actually works.
We can make a simpler analogy in that English
words are meaningless until they are defined.
>
The PTS connection of an expression in Q to
its axioms Q is analogous to the connection
of an English word to its definition.
>
A proof merely looks to see if a definition
exists and if it does not then the English
Word / Expression of Q remains meaningless.
That's not what PTS says; that's simply you.
>
There is a difference between meaningless and wrong.
>
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
>
Olcott's Minimal Type Theory
G ↔ ¬Prov_PA(⌜G⌝)
Directed Graph of evaluation sequence
00 ↔ 01 02
01 G
02 ¬ 03
03 Prov_PA 04
04 Gödel_Number_of 01 // cycle indicates no well-founded justification tree exists.
That's completely nonresponsive. You're simply copying and pasting text from previous posts without any explanation of how you think it relates to the point I made (which you disingenuously snipped).
>
The Liar's Paradox isn't what I am discussing. I am discussing the fact that 'no number is equal to its successor' can't be proven in Q. That statement has absolutely no similarities to the Liar's Paradox.
>
André
>
Proof Theoretic Semantics rejects expressions
as Proof Theoretic Semantically incoherent.
Les messages affichés proviennent d'usenet.