Logic - 2016-08-17 (page 3 of 3)

In classical logic "forall x in S ( P(x) )" is equivalent to "forall x ( x in S implies P(x) )", so you can use your understanding of vacuous implication to understand vacuous universal quantification.

The reason I avoided this earlier is that in non-classical logic the game semantics may still hold but this equivalence might not.

toto

oh, cool

user21820

And by the way that's why "f(0)=c" is outside of the "forall n ( ... )"

(answering your "does not depend on n" question)

toto

okay so

it's like f(0)=c is not in P

user21820

4:15 PM

Yes it's not.

toto

so it's like

user21820

the game for "P and forall x in S ( Q(x) )" consists of two parts.

toto

forall n in N<k, (P(n)^f(0)=c)

user21820

First part is Prover shows P. Second part is Refuter starts and gives some x in S and Prover shows Q(x).

Your proposal is not equivalent.

Specifically if S is empty then "forall x in S ( P and Q(x) )" is true but "P and forall x in S ( Q(x) )" may be false.

toto

well, that's great because now i understand vaccuous truth by you equivalence "In classical logic "forall x in S ( P(x) )" is equivalent to "forall x ( x in S implies P(x) )"

user21820

4:19 PM

Lol. I thought you already understood it by the game semantics, which is really more fundamental.

toto

yes, too

user21820

You see classically we also have "exists x in S ( P(x) )" equivalent to "exists x ( x in S and P(x) )".

toto

but it was note based on something "hardware" like implication

user21820

There's a weird phenomenon here. One uses "implies" and the other uses "and".

That's why I say the classical equivalents are clearly not fundamental.

toto

hum

user21820

4:21 PM

Also, we have "neg forall x in S ( P(x) )" equivalent to "exists x in S ( neg P(x) )" (you can check that game semantics explains it).

toto

well okay

user21820

This duality is ugly when you convert to the classical equivalents.

toto

so, from that, we can say that proving initialisation of P(0)

is about proving f(0)=a

user21820

Yes.

toto

so proving that f contains (0,a)

right ?

user21820

4:23 PM

Yes, after you have given f.

which clearly can be constructed as {(0,a)}.

So done.

toto

yes

so that means that

fir i set f as f := {}

then i build (0,a) from N and the element a from E

then i do singleton on (0,a)

{0,a}

well okay neverwind

user21820

{(0,a)}

toto

i build (0,a)

user21820

and then you add it to f.

toto

then i use the singleton axiom on (0,a)

which gave me {(0,a)}

and i name this set f

user21820

4:25 PM

Yes that's the mathematical way

toto

okay cool

user21820

The "adding it to f" way is the programmer way of thinking.

toto

so f(0) done

yes, you're right

user21820

Which is perfect but just not entirely in line with ZF set theory.

toto

yup, i see ^^

user21820

4:26 PM

Great.

I'll be going off soon.

toto

yes okay

user21820

Ping me here another day if you want to continue.

toto

no prob, you have well helped me, you're such a well teacher

user21820

I hope to teach one day. Good?

toto

so just for the main idea, the next steps are to suppose P(k) true

user21820

4:27 PM

Haha..

And prove P(k+1) which you've roughly found already via that construction process.

(teach officially)

toto

so, it means that from P(k) hypothesis, i can state that the equality f(n+1)=g(f(n)) is true ?

user21820

don't forget your quantifier

toto

yes

forall n in N<k, f(n+1)=g(f(n))

user21820

P(k) includes "forall n in N[<k] ( ... )"

Yes so you basically take the witness for P(k) and add a pair to it to get a witness for P(k+1)

toto

and so, this equality help me to construct the next ordered pair

user21820

4:30 PM

which you can prove is so because it already satisfies everything you want by P(k) except you need to check for n = k.

toto

add it to another function f' which agrees with f on [0...k]

user21820

Yup.

toto

then i can states that f' is my function which satisfies P(k+1) from P(k)

user21820

I think you can see where this is going already.

toto

So P(k) is true for every n naturals

user21820

4:31 PM

Yes.

toto

But, and the other step is to prove that every function f and f' which agrees on N

and have the same domain and range

are the same

so, it means that f = f' so this function is unique

user21820

you mean "which witness P(k)" not "which agrees on N"

toto

yes right

so next step ?

i've proved that f exist and is unique, that's ok no ?

user21820

Scroll back to the proof outline haha.

Anyway I think you'll find it easy to learn natural deduction (see those two links under my profile).

toto

okay

user21820

4:35 PM

That would make clearer one way to formally manipulate the existential quantifier. It's not a common way in mathematical logic but it is closest to how programming languages do it.

toto

don't see the links where are they ?

user21820

math.stackexchange.com/users/21820/user21820?tab=profile

under Fitch-style natural deduction

toto

Fitch-style ?

user21820

Fitch notation

Fitch notation, also known as Fitch diagrams (named after Frederic Fitch), is a notational system for constructing formal proofs used in sentential logics and predicate logics. Fitch-style proofs arrange the sequence of sentences which make up the proof into rows. A unique feature of Fitch notation is that the degree of indentation of each row conveys which assumptions are active for that step. == Example == Each row in a Fitch-style proof is either: an assumption or subproof assumption. a sentence justified by the citation of (1) a rule of inference and (2) the prior line or lines of the proof...

It's exactly what I've been using in our discussion.

toto

cool !

user21820

4:37 PM

You can just look at the examples I linked to, and it should be quite obvious how it is supposed to be.

Indentation is a significant invention of programmers

I'm sad that it hasn't caught on in mathematics.

toto

hum, that's cool

user21820

@toto: Okay enough for today. See you!