Logic - 2020-09-09

Threnody

04:39

@user21820
A formal system S is a triple ⟨L,T,C⟩ where L is a set of strings (of symbols over some alphabet) and T⊆L and C∈L. We will call L the language of S, and call T the theorems of S and call C a contradiction over S. We say that S is consistent iff C∉T. We say that S is computable iff L,T are computably enumerable sets.

Sorry I don't know how to 'quote'

I'm misunderstanding I bet, but : Shouldn't it be $C \subseteq T$? i.e. What's the idea behind considering one contradiction C instead of generalising to a collection of possible contradictions?

Another thing: Shouldn't the rules of deduction be crammed in there somewhere?

user21820

05:31

@Threnody Ah I see you noticed my recent post:

5

A: In what sense is $\sf ZFC$ "stronger" than Peano arithmetic?

Hanul Jeon gave a typical definition for "interpretation", but that is a rather restricted definition. In particular, it only applies for FOL theories. So for example we are unable to express statements like: Intuitionistic logic interprets classical logic (via the double-negation translation). ...

@Threnody To quote an entire post (question or answer) just paste the link to the post on its own in a chat message and it will automatically become a boxed format as above. To create a new text quote put > at the start of each line.

Threnody

@user21820 Oh I see

user21820

@user400188 @user76284: You may also be interested in the above post, where I (finally!) wrote out the specifics for what it means for one system to interpret another, especially when we also want to make sense of relative consistency even for non FOL theories.

@Threnody There's no need to generalize, because usually we only care that it does not prove some special sentence that we call a contradiction.

Threnody

@user21820 But what if that C is not in T, but some other $K = ¬T_i$ is?

user21820

@Threnody That is in fact permissible. This is a matter of preference. The whole point is that we do not want to restrict to FOL, so neither do we want to impose that "¬" is a symbol in the alphabet, not to say impose its meaning.

We could, of course, generalize to allow C⊆L∖T (which is what you should have written given your actual English inquiry), but then we would also need to generalize the notion of "consistently interprets", namely we would want to define that ⟨L',T',C'⟩ interprets ⟨L,T,C⟩ iff blah blah as before but ι(Q)∈C' for each Q∈C.

Gah I meant "C⊆L".

Obviously we hope C⊆L∖T as well, which would be what "consistent" would now mean.

Threnody

So the triple notation should be used when the deductive system used to obtain T is unambiguous?
> For example, an FOL system can be defined as a triple ⟨L,T,C⟩ where L is some set
> of sentences over an FOL language and T is a deductively closed subset of L
> under FOL deduction and C is the string "⊥".

lol...

user21820

05:45

@Threnody Yes that's why I wrote "deductively closed under FOL deduction".

You need a space after the >, and you need it on the first line too... And I think it cannot be a reply.

Threnody

Ah, alright

user21820

But it's actually an inconsequential generalization because the original definition is powerful enough to capture even that case! That is, given any generalized formal system X = ⟨L,T,U⟩ where U⊆L and U is supposed to be interpreted as a set of contradictions, let "☹" be a new symbol not in the alphabet A (L⊆A*), and let L' = (A⋃{"☹"})* and let T' = ( T⋂U=∅ ? T : T⋃{"☹"} ). Then S' = ⟨L',T',"☹"⟩ is a formal system (as in the original sense) that captures what you want.

Intuitively, this transformation takes any generalized formal system ⟨L,T,U⟩ and adds the rule that if you can deduce any member of U then you can deduce "☹" as well.

@Threnody And by "at the start of each line" I mean the actual line before the line-break. If you copy from within a single paragraph, then there are no line-breaks.

Threnody

I see what you're doing... so S and S' are both using the exact same underlying deductive system, correct?

user21820

@Threnody There's no reason to talk about a deductive system, because there may be none. There's just the set of theorems.

Although we often want to talk about computable formal systems where there is a deductive system, we don't have to.

Threnody

@user21820 How else do you obtain the theorems?

I understand that if I'm 'given' the theorems then I do not need to care about what deduction system was used

user21820

05:59

@Threnody It's given! It's just like a vector space comprises a field F and vectors V and ... You wouldn't ask how you obtain the vectors, would you?

Threnody

@user21820 Of course not :) I see.

user21820

It's just the definition. Whatever way people choose to construct ⟨L,T,C⟩ is up to them. It turns out that FOL theories have some nice properties, but other formal systems may not.

Threnody

> and let L' = (A⋃{"☹"})*

Does it need to be like this? Can't we just take L' = L⋃{"☹"}

user21820

@Threnody You can. I was just brainlessly doing the usual thing, which is to just have the entire lot of strings over the alphabet. =)

Threnody

Ok, thank you :) I have to study ODEs now.

user21820

06:04

Ok. See you next time! =)

user76284

07:41

@user21820 What does PA$^-$ stand for, again? Might be worth clarifying that in the post.

user21820

Peano axioms

In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are 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 th...

user76284

@user21820 I mean in contrast to PA.

Oh nevermind.

So PA without the induction schema.

user21820

Yup.

user21820

16:34

@MaliceVidrine: Lol I made some errors in that post but nobody noticed.

> any formal system that is consistently interpreted by some consistent formal system is itself consistent

Originally I wrote "that consistently interprets" lol..

> S≤S′ iff PA proves that S′ consistently interprets S.

Originally I didn't have "PA proves that", and I realize that it's necessary otherwise we get the trivial nonsense that if ZFC is consistent then I can just send every sentence except "⊥" to a tautology and claim that Z consistently interprets ZFC. Obviously, the catch is that PA is unable to prove that ZFC is consistent. In particular, if Z is consistent but ZFC is inconsistent then Z cannot consistently interpret ZFC.

So, good to check seeing I so frequently make mistakes... Incidentally I like this approach, since it does not depend on computable ordinals and weird encoding issues that arise with ordinal analysis, and yet seems to capture exactly the same hierarchy.

Cure

19:27

I have what I think is trivial question, but I cannot get my head around it. I'm reading about on Foundations of Math, and it starts with set theory, giving the ZFC axioms.

One of the goals of the ZF restrictions on set is to avoid the formation of bigger sets that lead to contradictions, like the one given by Russell's paradox, which ultimately leads to A∈A therefore A∉A , and if A∈A follows A∈A. But why is it a contradiction?

I now that intuitively always happens either A∈A or A∉A, but why does it need to be the case? And in which ZF axiom is this property implied?

Or, to put my question in different terms, what is the meaning of ∈? Should I take it just as symbol which has properties established by the ZF axioms? If so, how come properties related to the relation ∈ among classes are, in several books, established well before the ZF axioms.

Malice Vidrine

21:51

@Cure - The law of non-contradiction isn't the result of any ZFC axiom, it's a part of the underlying logic in which ZFC is formulated.

And sometimes authors will talk about \in before talking about the axioms because they're speaking informally about how the intuitive idea of set-membership ought to behave. In the formalized theory, it has the properties that the axioms impose.

Cure

22:24

But once in formalized theory, can anything in regards of \in be said before going into the ZF axioms?

For example, I came across this theorem: \forall x \forall y [x=y \implies \forall z( z\in x \iff z\in y )]

and it can be proved using only the axioms of equality (identity and substitution). However, the reciprocal requires the first ZF axiom

The used of \in in a formal proof confused me, as I expected its properties to be fully defined by the ZF axioms. When reading that proof, and even the theorem, the question that comes to my mind is What is \in ?

At the very start of the book I read they give me a language, two binary symbols we annotate as = and \in . But while there are axioms that explicit what is = (identity and substitution axioms for equality), there aren't that describe how is \in supposed to be used.

But a (apparently intended) formal proof is given for the theorem I wrote above.

Or might be my intuition that is misleading me, and at that stage I should see \in as just a symbol that relates two elements, and the former theorem is true regardless of whatever it comes to mean later?

(of whatever \in comes to mean later, which properties are imposed to it by ZF)

Malice Vidrine

22:52

@Cure - In your example, absolutely nothing is being posited of \in. It's just an arbitrary binary relation, and the result a purely logical truth. You don't need axioms to license you to use a symbol. You need axioms to give you anything other than purely logical truths.

You could put < or "is divisible by" or anything else in that example, and it will still be true.

If Carol Danvers and Captain Marvel are identical, then Carol Danvers has saved exactly the same people as Captain Marvel. :P

Malice Vidrine

23:09

Likewise, the statement "there exists a set of all x such that x\notin x," in its fully written out first order form, is inconsistent as a matter of pure logic. No axioms involving \in, except as instances of the axioms of pure first order logic, are actually involved.

Transcript for

♦ $Mathematics$ Logic

Transcript for

♦ Logic

♦ $Mathematics$ Logic