Logic - 2017-09-18

@LeakyNun We can't say much. The completeness theorem is non-constructive. Remember that we can't even explicitly describe one countable model of PA that isn't PA itself.

And we can get a non-standard model of PA via the completeness theorem.

By the extra constant-symbol thing.

Leaky Nun

what do you mean by we can't describe it?

user21820

No computable model.

Leaky Nun

what of it isn't computable?

user21820

11:23 AM

2 days ago, by user21820

There is a theorem that there are no computable non-standard models of PA. This means that there is no computer implementations of the domain and arithmetic operations that obeys PA but is not isomorphic to the standard natural numbers.

Leaky Nun

I don't understand why I can't just write a program that computes say x+2+x = 2x+2

user21820

You need to implement the arithmetic operations on the entire domain.

So before that you need to have a program that recognizes the domain.

What would you use for the domain? Maybe the strings 1,2,3,... and then c to denote some non-standard number.

Leaky Nun

I can just build new objects as I need them?

right

user21820

You can't, because you're supposed to recognize the whole domain.

Leaky Nun

but it's infinite

user21820

11:28 AM

Natural numbers are infinite.

But the standard naturals correspond to a computable model of PA.

Leaky Nun

you don't store a list of all natural numbers right

you use lazy evaluation right

user21820

Hmm you should learn some computability theory. =)

Nothing to do with lazy evaluation.

We say that a collection of strings is recognizable/decidable/computable iff there is a program that accepts all its members and rejects all other strings.

The program cannot not-halt.

Leaky Nun

right

so I just look for strings with x and + and - and whatnot

user21820

I said that you need a program to recognize the entire domain.

Otherwise you can't call it a computable model.

Leaky Nun

my program accepts string that looks like 3x+5

user21820

11:33 AM

What about 2^x?

What about 2^(2^x)?

Leaky Nun

and those

user21820

I presume x is my c?

Leaky Nun

hmm I see the point

right

user21820

Well I'm not sure what happens if you try to push your idea to the limit.

Something must break down somewhere because of the fact I mentioned.

Lol.

Leaky Nun

right

user21820

11:35 AM

Ah I know. It's the induction axiom.

See without it PA is called PA−.

Peano axioms

In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are a set of axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly unchanged in a number of metamathematical investigations, including research into fundamental questions of whether number theory is consistent and complete. The need to formalize arithmetic was not well appreciated until the work of Hermann Grassmann, who showed in the 1860s that many facts in arithmetic could be derived from more basic facts about...

Click to go to the axioms for PA−.

Leaky Nun

what is wrong with it?

user21820

And PA− has a computable model which is essentially certain kinds of polynomials.

Which is like what you're doing.

Leaky Nun

hmm

user21820

You can computably add/multiply/compare two polynomials in c, under the assumption that c is bigger than any natural.

But it's not a model of PA, because induction fails for this model of PA−.

(c+1) is neither even nor odd, but a theorem of PA says that everything is either even or odd.

Leaky Nun

c is even then

(then is c/2 even?)

user21820

11:38 AM

Wait I should not use "odd" here. Rather, "of the form 2k+1".

PA proves that everything is either 2·k or 2·k+1 for some k.

It also proves the same for 3·k or 3·k+1 or 3·k+2.

c+1 is not of the form 2·k+1, since you don't have a polynomial in c that witnesses the k.

Leaky Nun

ya my polynomials have rational coefficients now

user21820

I forgot to say that in this model the polynomials have integer coefficients, and the leading one is positive.

Leaky Nun

and c is divisible by every standard natural

user21820

If you have rational coefficients, then 1/2 is included.

But 0 < 1/2 < 1.

PA proves (by induction) that there is nothing between 0 and 1.

See there's nothing you can do to avoid the problem.

But it's fun to try.

Leaky Nun

it's a representation

my constant term cant be non integer

user21820

11:41 AM

Then something else fails, and although I have an idea I'm too lazy to figure out. Your turn!

Find some sentence that PA can prove (via induction) that is not satisfied by your new idea.

Leaky Nun

well

user21820

=)

Leaky Nun

2^x is not a polynomial :p

after that we have x factorial

user21820

You don't need 2^c.

Leaky Nun

and then etc

why not?

user21820

11:43 AM

Because you only need to support arithmetic operations +,·.

Leaky Nun

I can prove exponents via induction

encoding sequences is first order

i thought we went through that

user21820

You miss the point. You only need to implement + and · on your chosen domain.

So exponentiation is not the problem for your new idea.

You're going to have to think harder!

Leaky Nun

no induction?

2^x needs to be an object

but it is bigger than any polynomial

user21820

Oh that's what you mean? You're saying that since one can prove in PA via Godel-coding that there is some sequence of c powers of 2, and can extract that last power, therefore that final power must also be in the domain, which it isn't in our attempt.

I think that's fine, but a rather complicated solution.

Leaky Nun

correct :)

and then we got x factorial

you can't include them all

user21820

11:47 AM

Anyway, I think that rather complicated solution easily convinces you of the truth of the claim that there is no computable model.

Haha..

Am I right?

Leaky Nun

I already said I see your point like 10 minutes ago :)

btw have you ever used prover9/mace4?

user21820

No, I haven't tried the first one and haven't heard of the second one.

Leaky Nun

mace4 interprets theories

I can actually see the functions and objects

it comes with prover9

user21820

Interesting.

The webpage is taking long to load though.

Leaky Nun

e.g. here's how you build a non-abelian group

Assumptions:

x*(y*z)=(x*y)*z.
x*0=x.
exists y x*y=0.

Goals (this is what you want to build a model to provide a counter-example for):

x*y=y*x.

implicit for-all quantifiers

the objects are numbered from 0

(I don't have to write down "closure" because it is implied)

All functions must be closed

@user21820 are you here?

user21820

12:03 PM

I see.

I am doing something else at the same time, and was also looking at the screenshot wondering why you have "abelian" as a goal.

Before I came back to see your explanation.

Leaky Nun

oh ok

sorry

user21820

Thanks for sharing anyway. I wasn't aware of it.

Though I presume it can't do much more than brute-force computation?

Leaky Nun

so here's where I get my intuitions for a model

@user21820 you're right

and if the model is infinite, it's basically useless

you can only use prover9 in that case if you want to prove something

also, how prover9 proves things is quite interesting

because it assumes the negation of your goals and tries to find a contradiction

user21820

@LeakyNun This is a standard technique for theorem provers.

Leaky Nun

hmm

oh and existential quantifiers are treated like functions

as you can see, f1 in the above example

it means inverse (our third axiom)

user21820

12:09 PM

@LeakyNun This is called Skolemization, if you want to look up the term.

Leaky Nun

thanks

it calls it "clausify"

user21820

That theorem was a puzzle I couldn't solve when I first saw it on a test...

Leaky Nun

lol

how many years ago was it?

@user21820 next time you see it on a test, use prover9 :D

user21820

@LeakyNun I'm not aware of a university that allows students to use prover9 on a test! =P

Leaky Nun

lol

do you know how para works?

user21820

12:15 PM

@LeakyNun years ago.

I don't know what is para.

Leaky Nun

paramodulate

@user21820 everything is provable in an inconsistent theory :P

user21820

I see you use chinese. But your name isn't chinese?

Hahaha..

Leaky Nun

where do you see me using chinese lol

Leaky Nun is an anagram of Kenny Lau

user21820

@LeakyNun The dialog box in the screenshot.

@LeakyNun Yes I saw your username elsewhere.

It's not chinese eh?

Leaky Nun

Lau is a Chinese surname lol

user21820

12:37 PM

I know, but many people with English given names use English rather than Chinese by default. Haha..

Leaky Nun

@user21820 I don't get you

I don't have an English surname

I have a Chinese given name and an English given name

the latter of which is Kenny

user21820

That's what I said, yes.

But never mind.

Leaky Nun

and we use the English given name and the Chinese surname

at least that's what we usually do in Hong Kong

user21820

I see. Anyway I need to go off now.

See you next time!

Leaky Nun

ok, thanks for your time

user21820

12:39 PM

(I meant use English on their computer.)

(Of course, if you're in Hongkong then Chinese is the default I guess.)

Leaky Nun

I don't see where Chinese appeared in my screenshots...

oh, I see it now :D

Leaky Nun

1:18 PM

> We can have a model $M$ of ZFC, with an inner model $N$ of ZF, such that there is a $\mathbb{Z}/2\mathbb{Z}$-vector space $V\in N$ such that $(i)$ $N\models$"$V$ has no basis" and $(ii)$ $M\models$"$V\cong\bigoplus_{\omega}\mathbb{Z}/2\mathbb{Z}$".

This makes it clearer what inside and outside mean

(from here)

user21820

1:50 PM

@LeakyNun Well we can talk in terms of models and inner models, but that means you are talking from a third viewpoint, the 'true' meta-system. Namely, you are in MS considering a model M of ZF that has inside itself a model N of ZF. It is not exactly a minor issue; within ZF we can prove what I said about any countable model of ZF, but within MS you cannot necessarily prove that you even have a model M of ZF in the first place, not to say one that has an inner set model.

Leaky Nun

:o alright

user21820

Now it turns out that if MS is strong enough (say MS is ZF again!) then MS can prove that any model of ZF has an inner set model.

Leaky Nun

what is 1. x->y and y->z 2. x->z called?

user21820

But it still doesn't remove the requirement of assumption of existence of a model of ZF.

@LeakyNun I don't know a name.

Leaky Nun

what is 1. x 2. y->x called?

user21820

1:52 PM

@LeakyNun I have my own name for that; repetition/reiteration in subcontext.

Leaky Nun

hmm?

1. x
2. not y or x [or intro]
3. y->x [def of ->]

is this ok?

user21820

Here "y⇒..." says "If y then ..."; that conditional "If y" creates a subcontext, in which you can assert any statement that you have deduced outside that subcontext.

Leaky Nun

oh ok

user21820

@LeakyNun This is okay in classical logic but not okay in intuitionistic logic.

Leaky Nun

oh

user21820

1:54 PM

@LeakyNun <− Yet this holds in intuitionistic logic.

Leaky Nun

what the hell

user21820

It's very simple. If you've never heard of Fitch-style natural deduction, then it may be illuminating for you to take a look at it.

From my profile under "Natural deduction" see the following post:

3

A: Predicate logic: How do you self-check the logical structure of your own arguments?

Truth tables are not enough to capture first-order logic (with quantifiers), so we use inference rules instead. Each inference rule is chosen to be sound, meaning that if you start with true statements and use the rule you will deduce only true statements. We say that these rules are truth-preser...

There I describe my variant of Fitch-style ND. You can see immediately what is going on in the logical structure of a proof in this style.

Leaky Nun

thanks

user21820

@LeakyNun For your example it's simply as follows:

Leaky Nun

I need 1. x->y and y->z 2. x->z ;_;

user21820

1:56 PM

x.
If y:
  x.
y⇒x.

Leaky Nun

oh

user21820

@LeakyNun And for your other example:

x⇒y.
y⇒z.
If x:
  x⇒y.
  y⇒z.
  y.
  z.
x⇒z.

Leaky Nun

ah!

thanks

user21820

If you look again at the Hilbert-style rules for propositional logic, you will see that they basically capture the notions of reasoning with/under implication.

So everything is very clear from the Fitch-style presentation.

Leaky Nun

I'm not sure if your $\exists$elim is allowed in other styles

I mean, of course other styles has $\exists$elim, but not fresh variables

user21820

1:59 PM

@LeakyNun You are absolutely right. There are different ways to design the rules. Some systems are like mine, while others are not.

Here is a PDF summarizing a whole lot of them: ualberta.ca/~francisp/papers/pelletierNDtexts.pdf

@LeakyNun And in another post I gave a closely related sequent-style variant of ND that corresponds to the other usual kind of ∃elim rule:

2

A: Calculus of Natural Deduction That Works for Empty Structures

The easiest (and in my opinion cleanest) way to do this is to augment the context. In the sequent calculus you presented, you have the left-hand of the sequent being a set $Γ$ of formulae. Instead of that, you need to have set of sentences $S$ for axioms and a context chain $Q$. $Q$ is an ordered...

Leaky Nun

thanks

user21820

The reason is that having globally bound variables is a headache when you want to present it in sequent-style.

Leaky Nun

right

user21820

The reason I had it in my other system is that it was designed to be as user-friendly as possible, which means friendly for my use because I was the only one using it.

(Until I posted it on Math SE, that is.)

It mirrors how one instantiates variables in modern programming languages.

Leaky Nun

did you create that system?

user21820

2:07 PM

Yes haha. I learnt programming earlier, so when I decided to design a system to formalize my logical reasoning, that's the system I ended up with.

Leaky Nun

woah :o

user21820

The indentation obviously comes from programming, and the colon for contexts comes from Python.

Leaky Nun

is there a rule for changing the name of variables?

bound variables, of course

user21820

In practice, I of course use such variable renaming. I did mention a bit about it in that post:

> Renaming quantified variables are unnecessary but would significantly shorten proofs. With renaming rules and omitting the lines in square-brackets the proof is much cleaner yet still easily computer-verifiable:

Under "Example".

So in practice I would write the shorter version using variable-renaming, but technically such rules are superfluous.

Leaky Nun

I mean, in "natural" deduction

in practice i do whatever-the-hell I want

user21820

2:11 PM

Hahaha "natural deduction" is sort of an umbrella term for all such systems. If you're talking about well-known systems, it's true that most of them don't have an explicit rule permitting variable-renaming.

Leaky Nun

so how do I do that?

user21820

What you would do is to prove that you can use the other rules to perform suitable deductions in order to deduce the same sentence with the variables renamed.

More precisely, you show that every proof that uses variable-renaming rules can be transformed into a proof that doesn't.

That's what I meant by "superfluous".

Leaky Nun

when can I reuse variable names?

user21820

In different systems, it's different. In mine, you can use any unused variable name for a new universal context, but you can only use fresh names for existential instantiation.

Leaky Nun

you mean existential introduction?

user21820

2:17 PM

No I mean ∃elim.

∃elim: If we prove a ∃-quantified statement, we can use a new variable for a witness for it.

|∃x∈S ( P(x) ).
|...
|------------------------ (where y is a fresh variable)
|Let y∈S such that P(y).
|[y∈S.]
|[P(y).]

It's necessary that y is fresh so that you don't get trouble with y hiding as a bound variable in some previously deduced sentence.

Leaky Nun

I cannot for the life of me move 4 outside

context: this question

I suspect the question is wrong, as I have stated in the comments.

I'll justify 2.3.2 later, ignore it for now

user21820

@LeakyNun You have just found the discrepancy between the two major kinds of logic.

One assumes the universe is non-empty.

Leaky Nun

@user21820 wat

I've broken logic itself @_@

what an achievement

user21820

If you don't assume that, you can never deduce any existential statement without any axiom/premise that is an existential statement.

Leaky Nun

ok, just tell me how to continue

user21820

2:21 PM

Your first step needs to be to obtain some object.

Leaky Nun

wat

@_@

logic is borked

@user21820 how do you do that?

I've never worked with objects

user21820

If S:
  ∃x ( P(x) ).
  Let y be such that P(y).
  If S:
    P(y).
  S⇒P(y).
  ∃x ( S⇒P(x) ).
If ¬S:
  Let y be something.
  If S:
    Contradiction.
    P(y).
  S⇒P(y).
  ∃x ( S⇒P(x) ).
∃x ( S⇒P(x) ).

Above is a proof in Fitch-style.

Leaky Nun

what is the last step's justification?

user21820

LEM gives "S∨¬S.", which is valid for classical logic.

That and ∨elim gives the conclusion.

Leaky Nun

so it can't be proved in intuitionistic logic?

intuition-al-ist-ism-al-ic logic

user21820

2:29 PM

Hmm. Let me think about that for a bit.

Leaky Nun

ya, I figured that you would need not S -> that thing

user21820

Anyway note that my deductive system that I linked you to does not permit you to do the "Let y be something." part.

Because my system doesn't assume that the universe is non-empty.

But most modern logic textbooks define models to be non-empty.

Leaky Nun

I think I have seen the justification for the last step

user21820

And their deductive systems are for non-empty models.

Leaky Nun

but I forgot what it's called

I mean, it's informally called "proof by case"

user21820

2:32 PM

As I said it's ∨elim.

Leaky Nun

oh

user21820

disjunction elimination.

That's if you have LEM.

In this case actually we don't need LEM if ∃ is defined via ¬∀¬

Leaky Nun

...

you're making everything 100x more confusing

user21820

Hey you were the one who asked about intuitionistic logic.

I just gave you a clear-cut proof in classical logic, and you just had to ask about a non-classical logic!

Leaky Nun

hey you were the one introducing it

or else I would just break $\to$ into $\neg \lor$!

user21820

2:37 PM

Heheh.

Wait let me see.

Leaky Nun

now the universe is imploding into my brain

user21820

@LeakyNun Okay here's the trigger:

S ⇒ ∃x ( P(x) ).
If ∀x ( ¬(S⇒P(x)) ):
	If S:
		∃x ( P(x) ).
		Let y be such that P(y).
		If S:
			P(y).

		S⇒P(y).
		¬(S⇒P(y)).
		Contradiction.
	¬S.
	Let c be something.
	If S:
		Contradiction.
		P(c).
	S⇒P(c).
	¬(S⇒P(c)).
	Contradiction.
¬∀x ( ¬(S⇒P(x)) ).

Leaky Nun

trigger?

hey, stop using proof by contradiction :P

user21820

This is an intuitionistically valid proof of that theorem where ∃ is defined as ¬∀¬.

No choice. We need the principle of explosion here too.

Leaky Nun

is contradiction valid?

user21820

2:42 PM

When you get a contradiction, you can deduce the negation of the condition.

But no double negation elimination (DNE).

Leaky Nun

@user21820 under intuitionist logic?

user21820

Yes.

Principle of explosion is also permitted, which is deducing anything from a contradiction.

In intuitionistic logic, negation is not a toggle. ¬P should be understood to mean "P leads to contradiction".

And P⇒Q should be understood to mean "From a proof of P we can get a proof of Q".

So that's why principle of (ex|im)plosion is valid.

Because you're not supposed to be able to get a proof of contradiction.

Leaky Nun

heh

user21820

Anyway I really got stuff to do, so have fun thinking about these things while I'm far away from your brain. =P

Leaky Nun

ok, thanks for your time

user21820

2:46 PM

You're welcome!

Leaky Nun

3:10 PM

Yes; they are. The distinction is useful in order to separate classical and intuitionistic logic. With Double Negation or the Law of Excluded Middle, the two version are equivalent; in intuitionistiv logic, where DN and LEM do not hold, RAA does not hold also. — Mauro ALLEGRANZA Sep 12 at 6:07

@user21820 RAA does not hold in intuitionistic logic?

user21820

@LeakyNun Yes. From contradiction you get negation of condition, but you cannot remove negation from condition. It's easy to think using the BHK interpretation, where a proof is literally a program that transforms proofs of premises into a proof of the conclusion. So if you have deduced "( P implies false ) implies false" you literally have a program that transforms a proof of "P implies false" to a proof of "false". Does that give you a program that proves P? Not necessarily.

7

Q: Intuitionistic logic plus $A → B \lor C \vdash ( A → B ) \lor ( A → C )$

The following is a classically valid deduction for any propositions $A,B,C$. $\def\imp{\rightarrow}$ $A \imp B \lor C \vdash ( A \imp B ) \lor ( A \imp C )$. But I'm quite sure it isn't intuitionistically valid, although I don't know how to prove it, which is my first question. If my conje...

Read the answer for a brief explanation of how to reason about what is intuitionistically valid or not.

It's where I first learnt it. =)

Leaky Nun

3:28 PM

How do you model intuitionistic logic @_@

1

A: How to prove this sequent using natural deduction?

Using Natural Deduction: 1) $S \to \exists x \ Px$ --- premise 2) $S$ --- assumed [a] 3) $\exists x \ Px$ --- from 1) and 2) by $\to$-elim 4) $Pa$ --- assumed [b] from 3) for $\exists$-elim: $a$ is "fresh", i.e. having no free occurrences in the premise nor in the assumption [a] 5) $S \to Pa...

Is this proof wrong?

@user21820

user21820

@LeakyNun I think it is wrong...

Leaky Nun

@user21820 for the reason I stated?

user21820

I simply don't trust anything that I can't systematically convert to Fitch-style.

It's so easy to handwave anything.

Leaky Nun

lol

user21820

At some point you have to draw the line and say it's invalid because it's not clear what you're doing.

Leaky Nun

3:39 PM

so where is the line drawn?

user21820

Oh Mauro deleted it. He normally doesn't make mistakes so he must have realized it here.

Leaky Nun

what :o

user21820

@LeakyNun When logicians are doubtful of the correctness of a proof, that's where I draw the line.

Leaky Nun

@user21820 could you delete your comment?

user21820

Which comment?

Leaky Nun

3:41 PM

@user21820 oops, I interpreted "draw the line" literally

LEM is classical... — user21820 7 mins ago

user21820

@LeakyNun Yes I will delete it, since you've corrected it. The page doesn't auto-refresh so I didn't know you edited it.

Leaky Nun

thanks

user21820

@LeakyNun Anyway read Hanno's post and you'll know how.

Leaky Nun

@user21820 sorry, where?

user21820

The post I linked to.

Leaky Nun

3:46 PM

mind = blown

Leaky Nun

4:03 PM

1. A→B∨C [P]
2.* A [A]
3.* A→B∨C [1 R]
4.* B∨C [3 2 →E]
5.* B [4 ∨E]
6.* C [4 ∨E]
7. A→B [2 5 →I]
8. A→C [2 6 →I]
9. (A→B)∨(A→C) [7 8 ∨I]

@user21820 I don't see anything wrong with this...

wait, sorry, i thought it said "and"

nvm, ignore this

Leaky Nun

9:38 PM

0

A: Natural Deduction Problem: Predicate Logic with Identity in a Gentzen-style system

01. ∀x[Qx↔[∃y[[Rxy]∧¬[x=y]]]] premise 02. ∀xQx premise 03. ∃x∃y∀z[[z=x]∨[z=y]] premise 04. ∃y∀z[[z=a]∨[z=y]] assumption 05. ∀z[[z=a]∨[z=b]] assumption 06. Rcd assumption 07. ¬[c=d] assumption...

@user21820 my magnum opus :P

Transcript for

♦ $Mathematics$ Logic

Transcript for

♦ Logic

♦ $Mathematics$ Logic