Logic - 2017-12-16 (page 1 of 4)

Secret

01:27

@user21820 Ah I see, that's easy: Replace "not (A or not A)" with "not (not A or A)". This can still trigger the contradiction we need

user21820

03:21

@Secret Wrong. Your replacement is not permitted by the rules. You need to be much more careful with the rules.

Secret

If not (A or not A):                 [Given]
    If not A:                            [If-sub]
        not A                             [If-sub]
        A or not A                      [Or-create]
        not (A or not A)              [If-repeat]
    not not A                           [Contradiction]
    A                                      [Not-destroy]
    A or not A                          [Or-create]
    not (A or not A)                  [If-sub]
not not (A or not A)                [Contradiction]

There, or-create allows inserting sentences from the left or from the right

David Reed

@LastIronStar Regarding what I said yesterday about quantum. I didn't really fully appreciate the leaps that are made until the last couple of months, after having taken phys and chemistry, when I returned to study this more in depth. The assumption the answerer is talking about in his response to my question here is the exact same assumption that allows for quantum superposition:

4

Q: Boundary conditions for spherical harmonics

How does the constraint that the solution to $ \\ $ $$\left((1-x^2)y'\right)' - \frac{m^2}{1-x^2}y = \lambda y$$ $ \\ $ be square integrable on $[-1,1]$, force the solution to be bounded at $\pm 1$?

user21820

03:37

@Secret Perfect.

David Reed

@user21820 do you have a preference one way or the other for fitch vs sequent?

user21820

@Secret Just to comment; that is precisely why the Or-Intro needs both left and right. Otherwise some things you can't prove.

@DavidReed Sequent calculus (like Gentzen's LK) is very neat and tidy from a syntactic perspective.

However, the only practical system (for actual mathematical work) is Fitch-style.

Secret

hmm.. I am not familiar with a scenario in classical logic where "or" does not commute, but I guess starting with a more general condition is more desirable

user21820

@Secret The fact that we want Or to have its semantics such that it commutes tells us that the rule is okay. And it just turns out that we can't prove the commutativity of Or without having both left and right for that rule.

David Reed

@user21820 Just curious, I don't think I've ever gone through fitch. I studied two different systems in undergrad logic courses that seem pseudo-similar to it.

user21820

03:47

The point is that the rules are purely syntactic and do not 'know' anything, much less what "Or" should mean.

@DavidReed Curiously, I first met Fitch-style natural deduction in the CS discrete structures course in my first year of undergraduate.

And I realized it was exactly what I had been doing on my own for 5 years before that.

Secret

https://en.wikipedia.org/wiki/Noncommutative_logic
and google always give me weirdness, lol

user21820

Anyway here is a link to Gentzen's LK:

Sequent calculus

Sequent calculus is, in essence, a style of formal logical argumentation where every line of a proof is a conditional tautology (called a sequent by Gerhard Gentzen) instead of an unconditional tautology. Each conditional tautology is inferred from other conditional tautologies on earlier lines in a formal argument according to rules and procedures of inference, giving a better approximation to the style of natural deduction used by mathematicians than David Hilbert's earlier style of formal logic where every line was an unconditional tautology. There may be more subtle distinctions to be made...

That article gives an example proof of ( ( A → ( B ∨ C ) ) → ( ( ( B → ¬ A ) ∧ ¬ C ) → ¬ A ) ).

You can see that it is not very compact because there is a ton of repetition.

So, just to advertise Fitch-style proofs, I'll give mine!

Secret

My brain go BSOD whenever there are too many nestings

btw does equality make sense in Fitch style proofs. What is a rule for equality?

user21820

If A implies ( B or C ):
	If ( B implies not A ) and not C:
		B implies not A.
		not C.
		If A:
			B or C.
			If B:
				not A.
			If C:
				If A:
					C.
					not C.
				not A.
			not A.
		not A.
	( ( B implies not A ) and not C ) implies not A.
( A implies ( B or C ) ) implies ( ( ( B implies not A ) and not C ) implies not A ).

All I omitted were some of the lines given by the If-Sub and Repeat rules.

See it is so compact despite me not using the symbols.

Leaky Nun

@Secret ah, don't get ahead of yourselves; equality is first-order logic; we're only in zeroth-order logic

user21820

03:56

@LeakyNun He didn't know that lol.

Secret

yeah, I thought equality is a very primitative notation

user21820

@Secret It will come later when we extend to first-order logic.

Secret

ok

Leaky Nun

@Secret if you still want to know: reflexivity (x=x), symmetry (x=y -> y=x), transitivity (x=y -> y=z -> x=z), function substitution (x1=y1 -> x2=y2 -> ... -> xn=yn -> f(x1,x2,...,xn)=f(y1,y2,...,yn)), relation substitution (x1=y1 -> x2=y2 -> ... -> xn=yn -> r(x1,x2,...,xn) iff r(y1,y2,...,yn))

Secret

sounds fine to me. But anyway will focus on 0th order for now

user21820

03:58

@LeakyNun No need so complicated!!

Leaky Nun

@user21820 how would you say it?

that's how I was taught in the logic course

David Reed

@user21820 I'm familiar with sequent calculus. That is the inference system I am accustomed to for FOL. The other type of deductive system I like is found in this text here: amazon.com/dp/0078038197/…

Leaky Nun

normal languages

David Reed

you can see rules of inference in first couple of pages of preview. Not sure whether you would call that fitch style or not

user21820

@LeakyNun Only 2 rules are needed for equality; Intro and Elim. Intro is just "t=t" for any term t. Elim is just "t=u , P(t) |− P(u)" for any terms t,u and 1-parameter sentence P. There are some subtle syntactic rules to prevent variable confusion, but the idea is just that.

Leaky Nun

04:00

oh ha

leibniz equality rules

user21820

No it's not!

Leibniz equality is the backward direction.

Which cannot be stated in first-order logic.

Leaky Nun

what does |- mean?

David Reed

proves

user21820

Just short-form for saying given what you have written on the left you can write what is on the right.

David Reed

left side proves right side

Leaky Nun

04:01

oh

aha

user21820

@DavidReed That is indeed how it can be interpreted for Hilbert-style too.

Leaky Nun

so P(t) := t=t with some variable confusion gives you t=u, t=t |- u=t

user21820

@LeakyNun Yes, but there is no variable confusion.

What I meant is like a quantified expression.

Leaky Nun

@user21820 well strictly following your rules it would be u=u instead of u=t

user21820

@LeakyNun No it won't because the 1-parameter sentence P can freely specify where the parameter goes.

Leaky Nun

04:03

I still like my version better :P

@user21820 but how do you specify it?

@Secret which one do you like?

user21820

In this case: P(x) :≡ ( x = t ).

Then if you have "t=u" and "t=t" you have "P(t)" and hence can write "P(u)".

Secret

@LeakyNun I am ok with both, but I usually prefer more compact writing

Leaky Nun

aha

Secret

The same reason why I tend to use the symbol False instead of generating a contradiction

Leaky Nun

nice @user21820

David Reed

04:07

@user21820 While we're on the sequent topic: Interesting fact I came across r/e boolos and cut-elimination once, referenced here on Wikipedia:

For systems formulated in the sequent calculus, analytic proofs are those proofs that do not use Cut. Typically such a proof will be longer, of course, and not necessarily trivially so. In his essay "Don't Eliminate Cut!" George Boolos demonstrated that there was a derivation that could be completed in a page using cut, but whose analytic proof could not be completed in the lifespan of the universe.

user21820

@Secret You could just use "False", and then when @LastIronStar asks you for a proof you just systematically replace it everywhere with a suitable pair of contradictory sentences. =)

Leaky Nun

@Secret do you know that ¬x is just a shorthand for x→⊥?

user21820

@DavidReed Yup. Don't worry; the Fitch-style system I gave does not suffer that kind of blowup.

@LeakyNun It's not true in 3-valued logic.

Leaky Nun

@user21820 heh?

David Reed

In his book he proves completeness without it, then adds it as a sound rule in the appendix

user21820

04:09

@LeakyNun Yea if I don't say something that seems relevant, I often have good reason for it.

Leaky Nun

@user21820 well it's true for intuitionistic logic which is all that i care about :P

user21820

@LeakyNun If that is really all you care about, note that you can't prove the incompleteness theorems.

Leaky Nun

could you elaborate on how it is not true in 3-valued logic?

user21820

In 3-valued logic we still have the rule "not not P |− P".

Leaky Nun

I have to object to "still" :P

user21820

04:12

Um...

But at least for the rules I gave, we had the Implies-Intro rule.

Leaky Nun

@user21820 and then how is it not true?

user21820

If you let Q be the Quine paradox sentence, then you actually have:

If Q:
  Contradiction.

But "not Q" also leads to contradiction.

So "not Q" cannot be a shorthand for "If Q is true then False".

Leaky Nun

why not?

Secret

@LeakyNun Yeah, and I actually like that better because it easily made way into intuitionist logic and 3-value logics

LastIronStar

@Secret If you use false it makes the syntactic proof easier but for me, it makes the semantics harder to see.

user21820

04:16

@Secret I said already that his claim is wrong for 3-valued logic.

Secret

Oops

LastIronStar

I don't know if you are thinking the same way, what do you think? @Secret

user21820

@LeakyNun If you have your identification then you get the following proof:

If Q:
	...
	False.
not Q.
...
False.

Leaky Nun

aha!

by "quine paradox sentence" what do you mean?

user21820

The one in this post:

6

A: Is Godel's modified liar an illogical statement?

Your question has two main facets. The first is that you did not grasp the way logic does not fall to the liar paradoxes. The second is that there are deeper reasons as to why we have such apparently innocuous sentences in natural language that seem to defy assimilation into formal logic systems....

David Reed

04:18

lol

user21820

So if you want your identification then you must modify the Implies-Intro rule to only hold when the condition is boolean.

Secret

This is like the upteenth time you quote that MSE

user21820

@Secret I don't know why. It always comes up.

Secret

lol

Leaky Nun

@user21820 so Godel's sentence?

David Reed

04:19

@Secret that's what I was thinking. How leaky could have known him this long w/o having him bring it up at least 10 times :)

user21820

@LeakyNun Well Godel's sentence is qualitatively different, as sort of shown in the preceding part of that post.

The difference is that Godel's sentence does not refer to semantic truth.

So it escapes the problem of being potentially ungrounded (not boolean).

Secret

@LastIronStar I might write using false, but if you need clarification, I can rewrite the proof with contradictory sentences

Leaky Nun

@user21820 why do you not get the same problem with Q being Godel sentence?

oh, never mind

Secret

btw I am on mbobile for at least 2 hrs today, so I cannot type code fast enough

Leaky Nun

everytime I talk with you I learn how much I don't know @user21820

user21820

04:22

@LeakyNun Informally, it is because we assume that N is a fixed collection. So it sort of makes sense that quantification over it is boolean.

It just so happens that such sentences can be themselves encoded as naturals.

@LeakyNun You definitely know a lot of stuff I don't, such as all those prover toys you have been playing with.

@DavidReed @LastIronStar @Secret: In case any of you are interested, I'm referring to things like Mace and Prover9 that LeakyNun told me about.

Leaky Nun

@user21820 I'm sure you can learn it in a minute

user21820

Impossible. 60 seconds is too short.

Leaky Nun

if you insist

David Reed

Are those automated theorem provers?

Leaky Nun

@DavidReed the latter is

the former finds models

and you also have proof assistants such as coq

David Reed

04:26

from what I've read they are taking on a bigger and bigger role

Secret

One MSE user introduce something called IDE to check models

But I am not familiar with it yet

Leaky Nun

@Secret go learn first order logic first :P

LastIronStar

I think mechanical theorem proving is slightly above my current pay grade

Secret

Indeed

user21820

Lol.

Leaky Nun

04:33

ha!

p implies q is defined as p ≥ q right

Secret

NB, consider me semi afk cause mobile typing is too slow

user21820

@LeakyNun In 3-valued logic? Depends on which variant. Kleene's does not, but some others do.

Anyway let's go back to classical propositional logic.

Since everyone is here.

Define a propositional sentence (built from atomic (boolean) propositions and the connectives "not", "and", "or", "implies") to be a tautology iff it is true for every possible assignment of truth values to the atoms.

Leaky Nun

@user21820 hmm, I haven't explored much on modal logic

do you have some motivation for me?

user21820

@LeakyNun Well remind me next time, but provability logic, deontic logic, and necessity/possibility logic, at least.

Leaky Nun

and beginner exercises?

David Reed

04:41

I did a brief survey on it once and didn't find it very interesting

user21820

@LeakyNun Don't know of any; I learnt most of it on my own referring to random online sources.

David Reed

@LeakyNun I can post more screenies from same book on modal logic if you would like

Leaky Nun

hmm

LastIronStar

How is a tautology different from a theorem?

Leaky Nun

@LastIronStar that's what he's going to ask :P

user21820

04:43

A theorem is one that we can write a proof for.

Leaky Nun

theorem is syntactic

tautology is semantic

LastIronStar

@LeakyNun oh lol

user21820

Is it obvious to you that you can prove every possible tautology?

Leaky Nun

@LastIronStar the completeness theorem guarantees their equivalence

user21820

At least, it should be clear (from our goal) that every theorem is a tautology. So we have achieved a significant thing already.

@LeakyNun I will now sketch the proof of what is called semantic-completeness of this Fitch-style system for propositional logic.

It states the converse, namely that every tautology is a theorem!

Okay? @Secret, you're there, right?

LastIronStar

04:45

@user21820 The way i understand it now is that theorem is something that can be written outside any sub-contexts for some proof. correct?

user21820

Correct.

LastIronStar

which means that it is true regardless of context, that is it is true no matter what truth values you assign

user21820

Yeap. That's the reason why every theorem is a tautology.

LastIronStar

isn't that what you called as tautology?

user21820

It's only one direction.

LastIronStar

04:47

I see

user21820

Remember you asked what happens if we take away some rules?

Then the system will fail to prove some tautologies.

LastIronStar

@user21820 ok, continue

David Reed

no idea

@LastIronStar I can't speak for forallx's definitions but in my courses a tautology always referred to a statement that is always true irrespective of the truth values of it's atomic statement, a theorem is something that is a consequence of a given set of assumptions

user21820

@DavidReed I am not using forallx.

David Reed

ok

user21820

04:55

But yes your definition is okay, just must specify what "consequence" means, which of course must be some deductive system.

David Reed

atomic statements*

user21820

@LastIronStar Okay so remember that we had a theorem "A or not A."

Notice that we could use the same proof to get such a theorem for every atom, not just A.

That is the first step.

This theorem can be called an instance of LEM (law of excluded middle).

Secret

@user21820 So far ok, but I cannot respond as frequently as I can had I am in a comp

LastIronStar

@DavidReed oh ok

@user21820 I see

@DavidReed so when you write outside of any sub-context, it is sort of like there are no added assumptions right?

user21820

@LastIronStar Essentially right.

But I'll be using the Fitch-style system we've defined, so there will be slight differences.

LastIronStar

05:01

ok

user21820

→ 17 messages moved to Logic books

@DavidReed Okay so the messages related to this now have their own room to run about in, called Logic books. =)

@LastIronStar: Okay so let's go.

The idea is that whether a propositional sentence is a tautology can be checked by manually checking every possible truth assignment.

So all we have to do is to show that we can construct a proof that essentially does just that.

In our manual checking, we need to check 2 cases for each atom, and that is what we shall use LEM for.

We will also use structural induction on the length of the sentence. Do you both know what that is?

LastIronStar

@user21820 I know regular induction

Secret

I might need some recap of structural induction in a more concise form

user21820

Okay.

Structural induction basically says that if we can assign natural sizes to some collection, and we want to prove that every member satisfies some property P, then it suffices to show that ( if every member of size < n satisfies P then every member of size n satisfies P ).

LastIronStar

basically we are trying to show that if you can say a sentence is correct by checking all possible truth value combinations, then you can write that in the style of a proof?

user21820

05:10

Yes.

LastIronStar

ok

David Reed

@LastIronStar I'm actually not super familiar with the system that 820's taking you through, so I don't know what "sub-context means", the easiest way to get a feel for what a tautology is (at least for me) is that it is something whose column in a truth table consists of all T's. You can think of a tautology as something being proved from no assumptions, a theorem would require at least one assumption

The statement A or not A is a tautology, it is always true irregardless of whether A is true or false

user21820

@DavidReed Um the last part about "theorems" needing "assumptions" is incorrect.

LastIronStar

@DavidReed one sec, let me dig up the definitions of proof and theorem for you

@DavidReed A proof is a finite sequence of lines that can be written according to the rules. A theorem is a sentence that can be written in some proof under no context-header.

A context-header is any sentence of the form "If A:"

David Reed

Yes i should clarify that a tautology is technically a theorem

user21820

05:14

@LastIronStar Any line of the form "If A:".

David Reed

I personally don't think of it that way though

user21820

@DavidReed Yes but for the sake of analyzing logic systems, we're going to have to do it that way.

David Reed

lol

user21820

Here is a simple example. Suppose we want to prove Q, which you can check is a tautology.

Q = A or ( A implies B ).

A or not A.
B or not B.
If A:
	If B:
		...
		Q.
	If not B:
		...
		Q.
If not A:
	If B:
		...
		Q.
	If not B:
		...
		Q.

LastIronStar

@user21820 what is difference between sentence and line?

user21820

05:16

@LastIronStar I was just careful to say sentence only when it was a well-formed statement (like a proposition). The context-headers are not really sentences. Anyway such details don't matter much.

LastIronStar

@user21820 ok, this makes sense

user21820

I have just written an outline of the kind of proof we want to construct.

LastIronStar

@user21820 ok i don't know what you mean by well-formed, but let's leave it for now

user21820

I shall now fill in the blanks to show how it is done in this example.

LastIronStar

@user21820 yes, proof plan

Let me try to prove it.

user21820

05:18

Sure. Actually I missed out the important final steps:

A or not A.
B or not B.
If A:
	If B:
		Q.
	If not B:
		Q.
	Q.
If not A:
	If B:
		...
		Q.
	If not B:
		...
		Q.
	Q.
Q.

LastIronStar

@user21820 I thought you had done that on purpose lol

user21820

Lol no it's just that when I use my system in practice I don't bother writing the final steps.

LastIronStar

@user21820 "The rest of the proof is left as an exercise to the reader"

btw when you wrote Q = A or ( A implies B ), you assumed = is given but sometime back, I think @LeakyNun pointed out that = is first order logic, so how do we define something in our 0th order logic?

user21820

@LastIronStar That "=" was not inside the proof.

It was just for our convenience so that I don't have to keep writing the whole thing.

LastIronStar

ok

sort of like constant definition in C

user21820

05:22

Anyway I think it's better for me to give the filled-in version. You can try finding a different proof that does not go by splitting cases, but the one I'm giving really obeys the structural induction that we need.

LastIronStar

@user21820 oh ok

user21820

A or not A.
B or not B.
If A:
	If B:
		Q.
	If not B:
		Q.
	Q.
If not A:
	If B:
		If A:
			B.
		A implies B.
		Q.
	If not B:
		If A:
			If not B:
				A.
				not A.
			not not B.
			B.
		A implies B.
		Q.
	Q.
Q.

Secret

Given A, when using or-crest we can make A or B. Is B can be anything?

user21820

Well now that I think of it, using structural induction we don't actually have to split all the cases.

@Secret Yes.

Tell you what, both of you can compete to find the shortest proof of the theorem, while I go do something.

Leaky Nun

so I'm out?

user21820

05:24

Treat it as exercise for the earlier lesson.

@LeakyNun Ya you and David are out. You both can show yours after theirs if yours is shorter.

=)

I'll be back in about 20 min.

Secret

Ok

Leaky Nun

14 lines

I don't know the strict format that you taught though

user21820

05:41

@LeakyNun Well yea it may change depending on whether you omit the lines that are purely repetition. Typically I don't count them as they aren't really steps.

Leaky Nun

let's just say that spoiler is here for @user21820 to check

how many lines would that be in your format?

user21820

@LeakyNun Well you need to add a bit because you used explosion and I didn't actually have an explosion rule.

Leaky Nun

ah

LastIronStar

Sorry folks, I have some errands to run @user21820 you are free later today? I will work on the proof once i'm back

Leaky Nun

what is the non-intuitionistic rule that you have? only dne?

user21820

05:44

16 hours ago, by LastIronStar

1. Repeat:
| A
|---------
| A
2. If-sub
|
|---------
| If A:
|      A.
3. If-repeat
| A
| If B:
|---------
|     A.
4. Implies
| if A:
|     B.
|----------
| A => B.
5. Dual of implies
| A.
| A => B.
|-----------
| B.
6. And-create
| A.
| B.
|-------
| A and B.
7. And-destroy
| A and B.
|---------
| A.
| B.
8. Or-Create
| A.
|---------
| A or B.
| B or A.
9. Or-destroy
| A or B.
| If A:
|     C.
| If B:
|     C.
|---------
| C.
10. not-destroy
| not not A.
|------------
| A.
11. Contradiction
| If A:

It is surprisingly hard to find such kind of messages.

@LastIronStar Sure sure. No problem see you later!

Leaky Nun

11. Contradiction
| If A:
|     B.
|     not B.
|-------------
| not A.

user21820

@LeakyNun That is actually intuitionistically valid, it's DNE that's not.

Leaky Nun

I know, just that it got cut by SE

user21820

Oh.

Anyway I win you heheh..

Leaky Nun

sure

David Reed

05:50

@LeakyNun Are you a constructivist?

user21820

@LeakyNun: My solution here. I omitted exact repetitions.

David Reed

That is, do you reject

DNE and LEM?

Leaky Nun

yes and yes

:P

i only reject it for fun though

David Reed

I can't imagine what a nightmare real analysis would be for you :)

oh

gotcha

Secret

I don't like DNE after being made aware of intuitionistic logic

For LEM, I cannot comment because my thinking is subconsciously stubbornly fixated to it despite I try to break through

Leaky Nun

05:56

@Secret but they're equivalent under the other intuitionistic axioms

user21820

@LeakyNun Including Explosion. =)

Leaky Nun

...

are you a minimalist?

user21820

No, but it's just curious that you can derive one from the other without explosion but not the other way around.

Anyway, as I said, lots of basic computability results cannot even be proven in intuitionistic logic.

Like the halting problem cannot even be defined.

Secret

My current stances on infinity:
Potential infinity is necessary, actual infinity is necessary when dealing with nonstandard algebraic structures and analysis and other nonarchimedian algebras
Uncountable well orderings is an abstract art, thus it cannot exist except inside the Metropolis Algebra that I will soon built after mastering enough mathematics

user21820

@LeakyNun: So it's fine if you have a global non-classical logic but inside it you had better have classical arithmetic otherwise you really can't do anything much.

Leaky Nun

05:59

alright

Transcript for

♦ $Mathematics$ Logic

Transcript for

♦ Logic

♦ $Mathematics$ Logic