Logic - 2018-11-14

« first day (819 days earlier) ← previous day next day → last day (1987 days later) »

5:44 PM

@CarlMummert: So what do you think of the 'motivation' I gave for PA*?

@user21820 when proving Löwenheim–Skolem theorem we use choice, do we have to use choice, i.e. was it proven that it is improvable without choice?

user21820

@CarlMummert @LeakyNun: Also, for any explicit formal system S, we can define Con(S) as "∀p<M ( p is not a proof of (0=1) over S )", and this has the interesting feature of being compatible with the possibility that S is consistent in the sense of having no explicitly constructible proof of (0=1) and yet has no real-world model.

@Holo You only need a well-ordering of your non-logical symbols, and you can from consistency obtain a model. Namely, for any consistent first-order theory S and a well-ordering of non-logical symbols of S and a well-ordered sequence { c[i] : i∈I } of constant-symbols, you can prove the consistency of S + { c[i]≠c[j] : i,j∈I ∧ i≠j } and so construct a Henkin model by a transfinite induction along a well-ordering of sentences over the extended theory (by length then lexicographic order).

None of this requires AC. So the completeness theorem of a countable theory does not need AC. In general, you would get a model M such that C injects into M and M injects into N·C. I'm not sure whether that implies that M bijects with C.

Holo

6:10 PM

@user21820 I am not sure I understand how you prove like this that there exists smaller model of S

user21820

@Holo If S is countable and has a model, then it must be consistent, and then by what I said it has a countable model.

Holo

6:28 PM

Oh right! So why the usual way of proving it is to use choice to show (the downwards part) is to show that if I is a family of indexes and f[i] are functions then taking a subset of the model with size k then recursively adding the image of f[i] to the subset then the union of all of the steps will be of size k?

(the choice is because we are using k*k=k and after that part we use choice to create a function for each formula)

user21820

6:44 PM

@Holo I have never known that as the 'usual way'. Maybe it's because I always prefer proof-theoretic to model-theoretic methods. Haha..

Holo

@user21820 Well, saying "usual" because this is the way I first saw it is a bit off heh.

I think wiki also describes that way(although wiki is not the best source)

Löwenheim–Skolem theorem

In mathematical logic, the Löwenheim–Skolem theorem, named for Leopold Löwenheim and Thoralf Skolem, states that if a countable first-order theory has an infinite model, then for every infinite cardinal number κ it has a model of size κ. The result implies that first-order theories are unable to control the cardinality of their infinite models, and that no first-order theory with an infinite model can have a unique model up to isomorphism. The (downward) Löwenheim–Skolem theorem is one of the two key properties, along with the compactness theorem, that are used in Lindström's theorem to characterize...

Yep

user21820

@Holo Interesting that they did that when they didn't have to. The wikipedia page on the completeness theorem does say that it doesn't require AC.

Holo

7:17 PM

@user21820 here it says that for elementary submodel countable submodel we have to use some choice

« first day (819 days earlier) ← previous day next day → last day (1987 days later) »

all rooms