Re: arithmetic in ZF

> > Babylonian wrote:
> > > Classicaly, if we assume ~(Ex)Px and
> > > prove p&~p, we can infer (Ex)Px.
> > > THIS inference leads to belief in
> > > objects whose existence is
> > > "non-algorithmic and essentially
> > > unverifiable constructively",

george wrote:
> > Why "essentially"?
> > If you can prove p -> q then you ought to be
> > able to prove ~q -> ~p (it is equivalent).
> > In the case of Ex[Px] -> p&~p, the contrapositive is
> > (pv~p) -> ~Ex[Px],

I dropped a ~ there. The original context was, "if
we assume ~(Ex)Px". I said, "in the case of Ex[Px]".
I should've had the case of ~Ex[Px].
But classically,
~Ex[Px] is equivalent to Ax[~Px].
So, instead, let's start there.
Let's assume that we have derived Ax[~Px] -> p&~p.
What follows?
Well, both intuitionistically AND classically,
~Ax[~Px] follows.

> No, the contrapositive is
> ~(p&~p) -> ~Ex[Px] and the inference
> ~(p&~p) => ~pv~~p is not constructively valid,
> nor is the inference ~~p => p.

Right, and just as it is not intuitionistically
simple/deMorgan to deny binary 0th-order conjunctions,
it is not simple to deny the infinitary first-order-analogous
universal quantifier; we cannot get (intuitionistically)
from ~Ax[~Px] to Ex[~~Px], and even if we could, we could
not get from there to Ex[Px]. Classically, this chain is
easy: Ax[~Px] -> q&~q
int&cl=> ~Ax[~Px]
cl=> Ex[~~Px]
cl=> Ex[Px]
but intuitionistically, only the first link holds.
This proof is therefore non-intuitionistic, but why
is it also non-constructive? Because I was off by
one ~, I got correctly corrected this way:

> I do not deny that nonconstructive proofs can guide
> the search for constructive proofs - but in this case,
> all you have us doing is starting over and looking for
> a proof of > (pv~p)->~(Ex)Px.

Yeah, but that was by accident.

> We'd rather prove (qv~q)->(Ex)Px,

Right.
This is actually the case I wanted to be talking about.

> and prove q or prove ~q.


Let's take the contrapositive of that "shared first link"
above and begin by assuming we have a proof of
(qv~q)->Ex[Px], both intuitionistically and classically.
How do we get from here to Ex[Px] ?
Classically we get there trivially by LEM,
but if that is not available, how do we discharge the qv~q
hypothesis both intuitionistically and constructively?

The q arose out of a non-constructive proof and we begin
by asking if it provides guidance for an intuitionistic one.
The classical proof didn't produce Just Any old contradiction;
it produced one with specific relevance to the problem.
Is its relevance strong enough that ~q->Ex[Px] is provable?
If it is, then, classically, we might be able to do this by
cases instead of by LEM.
Having proved ~q->Ex[Px], you could then either
a) prove ~q, which would work both intuitionistically and
classically, or b) prove q->Ex[Px], which would not work
intuitionistically but would work classically.

My problem with calling one of these inferior to or less
constructive than the other is that I don't see how you
can dismiss the proof as non-constructive if both
q ->Ex[Px] and ~q ->Ex[Px] are constructive.
"Intuitionistic" and "constructive" are slightly different
notions here.

.

Relevant Pages

  • Re: Mavic
    ... Adding a simple element of causality: "Red skies at night... ... contradiction in terms) is that it accumulates all kinds of ... Of course without a causal model (perhaps a ... people who deny that for which they don't have a theory. ...
    (rec.bicycles.tech)
  • Re: arithmetic in ZF
    ... when you try to deny a universally quantified statement? ... formalism you like, because classically, they are all ... if Axleads you to a contradiction, ... it leads you to a particular ...
    (sci.logic)
  • Re: The Fundamental Flaw of SR.
    ... > the light in B's frame is not isotropic and B insisted that the light in ... *and* B are right - which is indeed a logical contradiction. ... observer independent reality exists and claim that "everyone has his truth", ... while others deny that contradictions exist or even deny the basic of logic ...
    (sci.physics.relativity)
  • Re: arithmetic in ZF
    ... > it is not simple to deny the infinitary first-order-analogous ... > The classical proof didn't produce Just Any old contradiction; ... but if you throw away the constructive proof of (q v ... The constructive proof gives us implicitly a witness ...
    (sci.logic)
  • Re: arithmetic in ZF
    ... >> objects whose existence is ... Proof by cases is an informal rule, not a formal rule, if it matters. ... > contradiction you derive may prove to be of some USE ...
    (sci.logic)
Quantcast