:: inaccessibility via barb ::

torkel franzen types:

:: I find it baffling that you read my comments as asserting that
theorem 9.9 doesn't prove anything. You're seeing conflicts where
none exist. ::

we have both used hyperbole
which is a great way to turn a serious discussion
into a vague diversionary argument without substance

so i apologise for that sentence
from my post

you actually "said" (on my screen):
"Theorem 9.9 is a characterization of the formulas provable in
intuitionistic propositional logic. It doesn't even have the
appearance of saying anything about arithmetical truth."

which i took as your way of changing the topic
from mine to yours
and avoiding explicitly admitting my initial assertion
(which you seem to agree is validated here)
by demonstrating your own goals
(re: arithmetical truth)
[[ and missing that it is about provability in PA ]]

there are moving targets here

anyway

:: The questions about the meaning of truth and provability
in intuitionistic mathematics that arise in this group from time
to time concern the foundations of the subject - how are we to
understand, let us say, an arithmetical statement when asserted
intuitionistically, or when assumed intuitionistically as a
hypothesis? Are such assertions and assumptions to be understood
in terms of proofs? ::


interpretational arguments
often evolve into
the game of philosophy

definitions get changed around
to keep an argument going

so its best to first agree
that the algebra is correct

once you have good structural agreement
the others interpretations seem
less foolish to each

barb knox recently brought up
a variant of S4
and asked how to interpret
the standard contraction on the diagonal lemma

maybe if i were to compare and contrast
using barb knox's question as a focal point
i might be able to
elucidate some interpretations

barb knox had asked:
[[ Someone please show me the error(s) in the following proof outline:

(1) Following Goedel, in Intuitionistic PA we can define the predicate
IPR(s) which is true iff s is the Godel number of a formula which has
some proof in Intuitionistic PA.

(2) Again following Goedel, in Intuitionistic PA we can construct a
formula G such that G <-> ~IPR([G]), where [G] means the Goedel number
of G.

(3) In Intuitionistic logic, phi <-> IPR([phi]). That is, a formula is
valid iff it has a proof.

(4) So by (3) and (2), IPR([G]) <-> G <-> ~IPR([G]), which is a
contradiction.

This is analogous to Tarski's proof that (classical) FOL can not define
its own truth function; except that Intuitionistic FOL *can* define its
own proveablilty function. Right? ]]

this can be interpreted
as a proof
that S4_HA is not
a provability logic for HA
(thus also PA)

i will use the translation

[]_HA F <---> provable_HA(|F|) <----> thereExists x, proof_HA(x,
|F|)

explicitly stating the logical calculus
here only

the above maps
IPR(s) -> [] S

which gives us 1)

2) the interpretation gives

thereExists G
(we can construct a G in HA)

G <-def-> ~[]G
or
G <--> ( []G -> _|_ )

(that is not provable in HA
where _|_ is the inaccesible)

3) the interpretation gives
if G is provable then G is true

[]G -> G

plus necessitation

|- G
------
|- []G

thus

4) thus

G <-> ~G

the liar

so S4_HA cannot be
a consistent provability logic of HA

this is actually a particular case
of a larger theorem

S4_HA cannot be
a consistent provability logic
of any system
that cannot prove its consistency

this is because of the behavior
of the inaccesible
with the modality

1) the provability of the inaccesible
is inaccesible

[]_|_ -> _|_

implies

~[]_|_

the inaccesible is not provable

thus when the S4_HA system derives

[]( ~[]_|_ )

by its axioms

it is provable that
the inacessible is not provable
and we have proven consistency

something not possible for HA
or PA

thus a truth in S4_HA
cannot consistently correspond
to a proof in HA

but we can keep the implication fragment IPC
and look at the traditional S4
(which we could write S4_PA in the above notation)

since

IPC |- F <==> S4 |- t(F)

where t(F) is the
famous "box all subformulas"
embedding

truth valuations of these two systems correspond

so if we could find a system where a statement in S4

[]F

corresponded to thereExisting a proof
of the interpretation of F in that system

then you could assert

when a valid proposition is given in IPC
thereExists a proof in that system

but S4 is in PA
and early constructivists saw the embeddability
of HA in PA as expressing some kind
of constructibility of proofs in PA

artemov showed that these past few
thereExists were the sickness that
inhibited relations with PA

he pulled a trick from skolem
and named a term
instead of asserting its existence

and created the system of LP
whose ontology consists of
statements in PA
and proofs of those statements
(named by proof polynomials)

then he proved realisability
of those LP terms
over S4 modal provability
in PA

it answers constructivist feelings
that a constructive proposition means
you can classically prove all subformulas

now if you want to discuss HA
we can move on to IBLP

but i think it is wise to stop here
and see if i am even close
to the
(moving)
target

-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
galathaea: prankster, fablist, magician, liar

.

Relevant Pages

  • Re: What is the intuitive meaning of Goedels undecidable statement?
    ... formalization. ... No interpretation needed. ... and 'truth' by 'provability' and 'provable' under the interpretation. ... Godel's undecidable wff. ...
    (sci.logic)
  • Re: Goedel - interesting problem?
    ... > gives us is an implication (if T is consistent then G). ... > A philosopher, Graham Priest, has argued that there is a formal theory T ... > claimed that the provability in would then refer to provability in ... > these are the only things that Gödel's theorems and Tarski's theorems ...
    (sci.logic)
  • Re: Goedel - interesting problem?
    ... >>Assume T is a consistent theory containing elementary arithmetic, ... inconsistent, which is why I wouldn't "accept" these schemata. ... The notion of "provability in T" can be represented in T containing ... these are the only things that Gödel's theorems and Tarski's theorems ...
    (sci.logic)
  • Re: What is the intuitive meaning of Goedels undecidable statement?
    ... and 'truth' by 'provability' and 'provable' under the interpretation. ... all the theorems of second-order Peano Arithmetic are not ... CB>> We can't prove the wff is unprovable within the logic, ...
    (sci.logic)
  • Re: Why is Cantor a target for cranks?
    ... distinction between provability and truth in an interpretation. ... The way NAFL works is as follows. ... this declaration in my mind. ...
    (sci.logic)
Quantcast