On 6/27/2026 1:53 AM, Tristan Wibberley wrote:It comes close. If ∃x x=S(x) is likewise "ungrounded" but in theOn 20/06/2026 18:32, olcott wrote:If there is no sequence of inference steps in Q from
>A proof theoretic expression is known to be true when>
it is fully grounded in its atomic base. Only two
PTS semantics researchers deal with true Dag Prawitz
is the one that began this. PTS previously only dealt
with semantic meaning and never got around to true(L,x).
That's surprising, disregard for axioms?
~∃x x=S(x) to the axioms of Q then ~∃x x=S(x) is
ungrounded in the PTS atomic base of Q.
This does not mean undecidable or incomplete
it means that ~∃x x=S(x) is out-of-scope for Q.
language of Q then ~∃x x=S(x) and ∃x x=S(x) are both undecidable
and Q is incomplete, bcause that is what the words mean.
--
Mikko
Les messages affichés proviennent d'usenet.