Logic - 2018-02-17

user21820

03:15

@skullpatrol Fine too! Busy period for me has just concluded a few days ago. =)

@LeakyNun: Hey finally I catch you in here. How are you?

Leaky Nun

@user21820 hi

user21820

Do you understand the distinction I'm making between the type ( nat → bool ) and the much smaller subtype of programs of that type?

Leaky Nun

yes

user21820

So which one did you actually want?

Leaky Nun

let's say the programs

user21820

03:21

Ok then I don't see an easier way for programs than constructing a Turing-complete language of some sort with an encoding of those programs into the type of inputs they accept.

Leaky Nun

ok

user21820

I'm not sure how easy it is in my type theory, though, and whether I can make use of the universal type.

One primary reason for having the universal type was precisely so that the procedures that do not invoke quantification or equality exactly correspond to ordinary programs.

And so that things like the fixed-point combinator works in greatest generality.

It's conceivable that one can hence cut out a subtype of proc(obj,obj) to represent programs.

Since any such object would itself be an obj.

But I'm not sure; never really tried. But if it works that might be quite neat.

If you want to work in a conventional foundation, then the best way is probably via tuples of naturals.

yesterday, by user21820

@LeakyNun: I think it's best if you have a type theory with inbuilt tuples, so that you can consider natural tuples, say ntuples, and consider a program as an ntuple that can be interpreted as proc(ntuple,ntuple). So you would have to construct that interpreter. Then you can talk about program behaviour.

Namely, you construct a finite set of programming primitives that allow you to compose arbitrary programs, and then encode them via tuples, and also define an interpreter for them.

If you do it in a manner compatible with your type theory, then you can get programs to be a subtype of proc(ntuple,ntuple), so that oracle programs would be trivial to define in that same type, making the whole thing quite clean.

user21820

03:45

@LeakyNun: I think even in my type theory there is no trivial way. One still has to allow programs to output code, not extensional objects.

Leaky Nun

yesterday, by user21820

@LeakyNun: I think it's best if you have a type theory with inbuilt tuples, so that you can consider natural tuples, say ntuples, and consider a program as an ntuple that can be interpreted as proc(ntuple,ntuple). So you would have to construct that interpreter. Then you can talk about program behaviour.

could you expand on that?

user21820

@LeakyNun Basically, define a certain kind of tuples of nat to be programs, which encode the primitives you want.

I presume you want natural arithmetic. And more importantly you need to have a way to compose programs and to perform recursion.

I suppose the bare minimum is to have the interpretation of programs to include ( ntuple x -> [0] ) and ( ntuple x -> [x[0]+1] ) and be closed under composition and recursion.

Composition is easy. If f,g are program interpretations then ( ntuple x -> f(g(x)) ) also is. Recursion is a bit more tricky.

I think the following closure rule should suffice:

If f,g,h are program interpretations then there is a program interpretation r with the same behaviour as ( ntuple x -> ( f(x)=[] ? g(x) : r(h(x)) ) ).

@LeakyNun: Do you think it is enough to cater for all kinds of recursion?

MatheinBoulomenos

04:00

hi @user21820

user21820

@MatheinBoulomenos Hello!

Leaky Nun

@user21820 how does the encoding work?

user21820

@LeakyNun So what I gave above are the interpretations. It is easy to choose some encoding of these into ntuples. You basically need to first encode a tuple of ntuples into a single ntuple. Once you have that, then you can encode each application of the closure rule using a tuple.

It's like encoding programs into code (symbol strings).

But if we do it using ntuples, then it is easier to write programs in this framework that manipulate programs.

Basically the first number in the encoding will tell you which rule is used, and then the rest of the tuple is to encode the contents that you apply the rule to.

Leaky Nun

I mean, I don't understand how you interpret ntuples as programs

user21820

Oh. Okay more precise:

[0] -> ( ntuple x -> [0] ).
[1] -> ( ntuple x -> [x[0]+1] ).
[2,code(f),code(g)] -> ( ntuple x -> f(g(x)) ).
[3,code(f),code(g),code(h)] -> ( ntuple x -> ( f(x)=[] ? g(x) : r(h(x)) ) ).

This is the interpretation function. The tuples on the left code for the program interpretations on the right.

The tuples on the left can further be encoded as just ntuples, so that they are compatible with the inputs and outputs of the program interpretations.

Well I guess we need a bit more closure rules to allow us to manipulate tuples.

@LeakyNun But do you get the idea?

Leaky Nun

04:10

so [1] is interpreted as the program that when given a program x, outputs the first number in x, add one?

user21820

Yup.

Leaky Nun

why?

and what is the r?

user21820

No particular reason; it's just that typically you need at least a constant, which [0] provides, and at least successor function or addition, plus recursion.

[3,code(f),code(g),code(h)] -> r where r has the same behaviour as ( ntuple x -> ( f(x)=[] ? g(x) : r(h(x)) ) ).

It's for recursion. We're basically saying [3,code(f),code(g),code(h)] encodes a recursive procedure r that is defined based on f,g,h.

And we need some more for manipulating tuples. I've not thought through this carefully but one should be able to do something along the same lines.

MatheinBoulomenos

@user21820 did you have a look at the book I mentioned? Using universal algebra to do logic sounds like an approach I'd like

user21820

04:29

@MatheinBoulomenos I glanced at it the last time. I just looked at it again. What do you want to know about it? I wouldn't recommend it as an introduction to logic, but by all means after you learn the basics you may find insights there. Personally though, I do not think logic should be treated as just a subfield of mathematics; it rightfully should be studied in a weak enough system for us to be sure that our theorems about logic are actually true.

MatheinBoulomenos

Hmm, okay, thanks for you opinion, I think I will start with Rautenberg, then

I'm personally not that worried about foundations, but I see why it is more important in logic than elsewhere

user21820

Foundations is indeed a tricky issue in logic. I don't even know the best way I'd like to go about it.

Many results do not require anything beyond a weak system of arithmetic called ACA. So it's worthwhile to not invoke higher set theory when proving those. However, there are some results that are proven in ZC (Zermelo plus choice), and it's not clear what to make of them.

@MatheinBoulomenos Concerning algebraic viewpoints, I think Rautenberg has quite a fair bit of it to satisfy you. =)

MatheinBoulomenos

Oh that sounds good

David Reed

I don't think we ever established whether you get Heine-borel on $\mathbb{R^n}$ with ACA

user21820

@DavidReed I was referring to "many results in logic". As for Heine-Borel, what version of it are you thinking of?

MatheinBoulomenos

04:43

I mean I'm fine that some theorems are statements about "theory of logic inside ZFC", just like theorems about groups are really statements about group theory inside ZFC. Once you look at infinite groups, the underlying set theory can matter critically

David Reed

I know. I was just remembering a conversation we had about its strength awhile back

It looks like you get it on the line with WKL

MatheinBoulomenos

(For some stuff i'm interested in, I'd actually prefer to even work with ZFC + the universe axiom, with iirc is equivalent to some cardinal stuff I don't understand)

user21820

@MatheinBoulomenos Exactly. It's quite interesting that the underlying foundations matter a lot when dealing with infinite collections, in part because in 'strong' systems such as ZFC the infinite collections are very 'powerful' (they cut the universe decidably into two pieces).

The problem is that when we prove "Formal system S proves sentence P.", we really really want it to be true.

We can't afford to have it be false (in reality), otherwise we're really doing nonsense.

It's equivalent to proving that a program halts when it never actually halts.

MatheinBoulomenos

I see

user21820

If ZFC plus whatever extra axioms you like is actually arithmetically sound, I don't actually have a problem with it.

The only problem is that I'm a bit doubtful.

MatheinBoulomenos

04:48

What does arithmetically sound mean?

Leaky Nun

it produces soundwaves that are arithmetic

so it may output an octave

user21820

We say that S (with a suitable translation ι of arithmetical sentences into it) is arithmetically sound iff ( for every arithmetical sentence P such that S proves ι(P), P is actually true in N ).

Leaky Nun

where by "actually true" we mean our intuitive interpretation of the natural numbers, i.e. the "standard model" of Peano Arithmetic

user21820

Here "arithmetical sentence" is a first-order sentence in the language of arithmetic, namely using only the symbols 0,1,+,·,< plus brackets and quantifiers.

Leaky Nun

and no logical connectives :P

user21820

04:51

Har har.. Of course plus logical connectives.

Leaky Nun

@user21820 0,S,+,·,< ...

user21820

@LeakyNun No need for S.

Leaky Nun

it's the standard language :P

user21820

I prefer the discrete ordered semi-ring axioms.

Leaky Nun

I don't

skullpatrol

04:52

what about =?

user21820

I like algebraic viewpoints when they fit nicely. @MatheinBoulomenos

Leaky Nun

@skullpatrol yes, and also variables...

user21820

@skullpatrol That too. In modern presentations of logic people usually assume equality is part of first-order logic.

@MatheinBoulomenos: For reference, the axioms for PA that I prefer are given at:

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...

@LeakyNun: There is a logic reason for preferring them too. PA− is defined solely in terms of the algebraic axioms.

And PA− is important in proof theory because it is finitely axiomatized and strong enough to do lots of arithmetic and forms the basis for a hierarchy of weak systems between it and PA.

skullpatrol

@user21820 how can it not be assumed?

user21820

@DavidReed I'd have to think about it; it's been some time since I thought about Heine-Borel. I recall that there was a significant jump from 1d to 2d, but thereafter it was easy.

Leaky Nun

04:57

@skullpatrol well, languages with equality are called "normal languages"

user21820

@skullpatrol Some older presentations do not include equality in first-order logic, in which case one has to add a predicate symbol for equality if one wants it.

skullpatrol

Thanks guys.

David Reed

@user21820 It would be interesting to see, in the realm of reverse mathematics, how necessary Heine-Borel is for analysis on $\mathbb{R^n}$. If you are able to find it I'd be curious to know

user21820

Let's call this weak first-order logic. Then every first-order theory T has a corresponding weak first-order theory T' where we take the usual axioms and add axioms for = to be a reflexive symmetric transitive relation.

MatheinBoulomenos

I think the way in which universes gets used in homological algebra and category theory is mostly to simplify the necessary bookkeeping. For example I want to say something like, the association taking each ring $R$ to the category of $R$-modules is a functor, because it is a natural thing to say, but there are several problems here.

user21820

04:59

Then every model of T easily translates to a model of T'. In the other direction, every model of T' can be collapsed by the equivalence relation induced by = to a model of T.

MatheinBoulomenos

Which is the category that this functor should go to? We can make sense of "The category of small categories" without universes, but the problem is that the category of $R$-modules is not small, so this doesn't work

The thing is, although the categories that we're interested in, like $R$-modules are not small, I've never seen a single argument which involved so many different objects that we couldn't just restrict ourselves to a suitable small subcategory

user21820

Yea.

But it feels like a hack, doesn't it.

MatheinBoulomenos

It feels like a hack

And even if I do that, I still can't really make sense of the statement that R -> R-mod is a functor

user21820

That's one of the reasons I don't like ZFC; it doesn't seem to be as general as it was originally intended to be, and in a technical sense it can never be, since we can always 'go one level up' and face the same problem.

MatheinBoulomenos

If I use universes, then everything works smoothly and there are no hacks to do

user21820

05:04

@MatheinBoulomenos Hmm I don't think so. It works for the stuff you've been doing, but I'm sure if you try you'll easily find a way to go up one level.

MatheinBoulomenos

Maybe if you do serious set theory or something like that

user21820

Haha I found this post that sort of captures the idea that Grothendieck universes is just like trying to iterate the idea of classes all the way up.

11

A: Category theory from MK class theory perspective?

Morse-Kelley set theory doesn't seem adequate for all the things one would like to do in category theory. It provides a nice treatment of proper classes, so it can deal with large categories like the category of sets or the category of groups. It can deal with a functor between two such categorie...

So I suppose you should be safe for all your 'practical' purposes. =)

MatheinBoulomenos

I don't feel to bad working with "stronger foundations", though as I said, if I really want I can break down the argument to something less elegant with more bookkeeping and possible hacks and it will work in ZFC

user21820

Yea that's not a problem, as I said, as long as you believe the foundations are arithmetically sound.

I should say that there is philosophical distinction to be made here. Just now I defined "arithmetical soundness" with respect to N, and @LeakyNun said it's what we intuitively believe the natural numbers are (in reality). That is the philosophical justification for why we want a foundational system to be arithmetically sound. There is a mathematical justification for a mathematical version of that, as well.

The mathematical version is to use the N given by the foundational system itself!

Namely, say we have a foundational system S and we want to know whether it's a good idea or not.

We surely expect S to have access to (prove the existence of) a model of PA, which we call the standard model N. (So this N is what S 'thinks' is the 'real' naturals.)

So now we can define (within S!) that S is arithmetically sound iff every arithmetical sentence that S proves is actually true of N (what S thinks is the naturals).

And then we can ask whether S proves that S is arithmetically unsound.

That, if true, would undermine all our confidence in S.

For ZFC specifically, the question is whether ZFC proves that ZFC is arithmetically unsound (according to itself).

MatheinBoulomenos

does it?

or is that undecidable?

user21820

05:17

We don't know.

It is possible for ZFC to be consistent and yet prove itself arithmetically unsound...

MatheinBoulomenos

that's interesting

user21820

I actually believe ZFC is consistent, but I doubt it's soundness.

And there is a strict hierarchy of soundness, which I recently showed using the computability viewpoint of the incompleteness theorem.

*its

There's another interesting issue as well. ZFC proves the existence of the real numbers, right?

Meaning, a structure satisfying the field axioms and the second-order supremum axiom.

MatheinBoulomenos

what's the issue with that?

Leaky Nun

yesterday, by user21820

Let t = ( nat n -> true ).
Let f = ( nat n -> null ).
If func(nat,bool) in class:
	t in func(nat,bool).
	If f in func(nat,bool):
		f(0) in bool.
		null in bool.
		null.
		null = true.
		false.
	not f in func(nat,bool).
	Let S = ( obj x -> ( ( nat y -> x in func(obj,proc(nat,obj)) ? x(x)(y) ) in func(nat,bool) ? f : t ) ).
	S in func(obj,proc(nat,obj)).
	S(S) == ( ( nat y -> S in func(obj,proc(nat,obj)) ? S(S)(y) ) in func(nat,bool) ? f : t ).
	== ( ( nat y -> true ? S(S)(y) ) in func(nat,bool) ? f : t ).

he proved, in his foundations, that func(nat,bool) (the type of all functions from nat to bool) is not a class

his foundation is even classical and has choice

well, the latter implies the former (diaconescu), but whatever

user21820

@LeakyNun Haha that's my type theory, but what I'm going to say is purely from ZFC's viewpoint.

Leaky Nun

05:26

alright, go on

user21820

@LeakyNun And remember I showed that Diaconescu's theorem doesn't work in my type theory. =)

@MatheinBoulomenos Firstly, ZFC proves that that (second-order) axiomatization is categorical; all models are isomorphic. Namely, there is a formula R over ZFC that is satisfied by the set of reals. Now, ZFC cannot prove that itself has a model, otherwise by the incompleteness theorem ZFC must itself be inconsistent. Therefore, ZFC cannot prove that itself has a model M that contains a set satisfying R with respect to M.

Secondly, if ZFC is consistent, then there is a model of ZFC where every set is definable, as stated here.

Thirdly, if we believe ZFC is meaningful we ought to believe that ZFC has a model M that has the same reals (contains a set satisfying R with respect to M). And the reals in M will be an uncountable set, so uncountably many will be undefinable over ZFC.

@MatheinBoulomenos: This is just interesting, not that it has any bearing on whether ZFC is a good foundation or not.

MatheinBoulomenos

I see

user21820

But if you look via my viewpoint, where I believe it is meaningful to have a universal type, then that is incompatible with any extension of ZFC, and something has to go.

Specifically, what @LeakyNun quoted shows that in my foundational system the type of real numbers cannot decidably split the universe into two pieces, meaning that membership in it is not necessarily boolean. Sometimes if you ask whether an object is a real, you will get no answer.

And this situation is in some sense necessary if you have a universal type and some other weak assumptions.

Leaky Nun

@user21820 for the love of God

> Sometimes if you ask whether an object is a real, you will get no answer.

hmm... :thonk:

user21820

Lol. It's the easiest way to explain it. =P

Okay maybe not.

@MatheinBoulomenos: Let's have a more precise explanation. In ZFC you assume that "x∈S" is always either true or false, for any objects x,S.

MatheinBoulomenos

05:36

yeah, LEM

user21820

In my type theory, and in general any type theory that has the universal type and some weak assumptions, that cannot hold for every x,S due to Russell's construction.

It turns out that more is true. We say that S is a class (what I earlier called having decidable membership) iff "x∈S" is always true or false for every object x. Even func(nat,bool), namely the type of all functions from nat to bool, cannot be a class.

skullpatrol

@LeakyNun is "no answer" the same as the empty set?

user21820

@skullpatrol It's the same as "null" in Kleene's 3-valued logic.

skullpatrol

So, the "null" set?

The set with no members.

user21820

No a third truth value. Basically, a statement either has a boolean truth value (true or false) or it has no value at all.

See plato.stanford.edu/entries/self-reference and search for "Kleene", but don't go to the linked article on many-valued logic, since Kleene's 3-valued logic is already defined there.

MatheinBoulomenos

05:42

So a type is to a class what a partial function is to a function?

user21820

@MatheinBoulomenos Absolutely right! That's how I designed my type theory.

skullpatrol

@user21820 ok, thanks for the link :-)

user21820

@MatheinBoulomenos Actually, if you're interested you can read the following post, which outlines the basic ideas behind my type theory:

1

A: Naively addressing Russell's paradox

What you are looking for is actually very elegant: 3-valued logic instead of classical logic. You are then free to construct a type given any defining formula, but membership may not be boolean. Call the types with boolean membership "classes". You can further stipulate that every type constructe...

And if you have any comments about the ideas I would be very interested to hear!

Leaky Nun

@user21820 instructions unclear; drown in the multitude of logicness

user21820

@LeakyNun What... I mean the first thing you might see when you search for "Kleene" is a link to "many-valued logic". I'm saying don't go there as you will drown in the many many-valued logics.

Leaky Nun

05:49

it's a joke

is there a type-theoretical interpretation of Kleene's 3-valued logic?

user21820

Lol.

@LeakyNun Hmm... not sure about that. I presume you're asking for something like BHK.

There is a problem though. As defined by Kleene, the 3-valued logic does not have any tautologies. This is obvious because null propagates.

In my type theory it becomes non-trivial because of the types overlaid onto the logic.

So we have tautologies like ∀P∈bool ( ¬¬P ⇒ P ).

But we do not have ∀S∈type ∀x∈obj ( x∈S ∨ x∉S ). We do have ∀S∈class ∀x∈obj ( x∈S ∨ x∉S ).

skullpatrol

> The mathematician and logician Kleene used a third truth degree for “undefined” in the context of partial recursive functions

> Blau (1978) used a different system as an inherent logic of natural language. In Blau’s system, both degrees 1 and ½ are designated. Other interpretations of the third truth degree ½, for example as “senseless”, “undetermined”, or “paradoxical”, motivated the study of other 3-valued systems.

user21820

@skullpatrol Yea. Since I intend for the logic to be applicable to reality, I do not consider paraconsistent systems to be meaningful.

skullpatrol

06:04

So, "undetermined" doesn't mean the same as "undefined"?

user21820

Well, I guess it depends on what you mean by them. Kleene's "undefined" (or my "null") is more like "no answer" (or "non-halting").

I presume some people might use "undetermined" to refer to something that has a truth-value but is undetermined?

MatheinBoulomenos

06:16

@user21820 this may be a dumb question, but when are two types equal in your type theory? A naive extension of extensionality seems problematic when membership is not decidable

user21820

@MatheinBoulomenos It's not a dumb question at all. You're correct that we cannot have naive extensionality. It means that equality too is not always decidable. If you can prove certain things, then you can prove equality between two types, or inequality respectively, and in some cases you can assert LEM for equality, but in other cases you just can't say anything at all.

MatheinBoulomenos

But do we have version that says if X and Y are classes then extensionality holds? iirc you can construct weird models of ZF - extensionality which we don't want

user21820

@MatheinBoulomenos Yes indeed classes satisfy extensionality in my type theory.

The intuition is that classes already decidably split the universe, and so whether they are equal or not is already 'decided' and cannot be changed.

MatheinBoulomenos

I see, that makes sense

user21820

If you compare to the Russell construction, it is like a recursive procedure that calls itself and attempts to say the opposite.

So you can't expect its value to be decided.

skullpatrol

06:28

Why did you use "<" here instead of "="?

2 hours ago, by user21820

Here "arithmetical sentence" is a first-order sentence in the language of arithmetic, namely using only the symbols 0,1,+,·,< plus brackets and quantifiers.

user21820

@skullpatrol Normally, "=" is part of first-order logic so we don't include it in the signature of the language. "<" is not necessary, but is convenient for the axiomatization of PA− that I prefer.

Discrete ordered semi-ring.

skullpatrol

Interesting

Thank you for your time and patience :-)

user21820

@skullpatrol No problem. If you have more questions you should just ask. I'm rather free these few weeks. There is really a lot that can be said about these weak theories of arithmetic. =)

skullpatrol

Will do.

MatheinBoulomenos

@user21820 since your type theory doesn't satisfy LEM, a natural question to ask seems to be if it satifies some kind of double negation elimination

But I'm not sure what a tautology should be when we have undecidable things

user21820

06:38

@MatheinBoulomenos Like Kleene's 3-valued logic, it does have DNE, unlike intuitionistic logic, because true/false are truly dual. Namely, we have the inference rule that if you have deduced "not not P" in some context then in that same context you can deduce "P".

MatheinBoulomenos

Ah I see, so it's not intutionistic

user21820

It does not matter that P could be null. The point is that the only possible situation where you can deduce "not not P" is in fact (by definition of "not") when P is true.

@MatheinBoulomenos Tautologies in my system must be quantified statements. In general, I do not allow any free variables.

For example: "forall P in bool ( P or not P )" is a theorem/tautology.

MatheinBoulomenos

okay that clears my confusion on tautologies

MatheinBoulomenos

06:56

@user21820 that was very interesting, thanks :) I'm off now, but since I now have semester break and the exams are over, I'll (finally!) get around to read Rautenberg, that will likely make me come up with lots of questions

user21820

@MatheinBoulomenos Sure. You're welcome!

MatheinBoulomenos

See you

skullpatrol

cya

user21820

@MatheinBoulomenos See you next time!

user21820

09:25

@DavidReed So can you be precise about which version of Heine-Borel you want? The Wikipedia page says that WKL0 is equivalent to "The Heine–Borel theorem for the closed unit real interval, in the following sense: every covering by a sequence of open intervals has a finite subcovering.". That version makes sense because we can talk about (countable) sequences of open intervals.

It also says that WKL0 it is equivalent to "The Heine–Borel theorem for complete totally bounded separable metric spaces (where covering is by a sequence of open balls).", but I've no idea what on earth that means (we can't talk about any arbitrary metric space in ACA, much less WKL0). But a version I am sure is provable is:

user21820

15:46

> Every sequence of open balls in R^n that cover the (n-dimensional) unit interval U has a finite subsequence that covers U.

Firstly, note that we cannot talk about uncountable collections in ACA, but it is clear that any finite cover of the rationals in U is also a cover of U, since it has a minimum ball radius, and the rationals are dense in U.

Secondly, the proof of what I stated goes as follows. Take any sequence B of open balls that cover U. If no finite subsequence of B covers U, then we can construct a sequence of intervals as follows. Let S[0] = U. For each natural n, divide S[n] into 2^n equal subintervals, and let S[n+1] be one of those subintervals with infinitely many points not in any of the first n+1 balls in B (or the subinterval nearest the origin if there is none).

Sorry.

Take any sequence B of open balls that cover U. If no finite subsequence of B covers U, then we can construct a sequence of intervals as follows. Let S[0] = U. For each natural n, divide S[n] into 2^n equal subintervals, and let S[n+1] be one of those subintervals that cannot be covered by any finite sequence of balls in B (or the subinterval nearest the origin if there is none).

user21820

16:13

Then prove by induction that S[n] has infinitely many points not in any of the first n balls in B. The induction step is not hard; if every subinterval of S[n] can be covered by some finite sequence of balls in B, then S[n] also has a finite subcover from B, contradicting the assumption; hence some subinterval of S[n] cannot be covered by any finite sequence of balls in B.

Now note that S[n] has diameter 2^−n, and hence we can construct the point p in the intersection of S. Then some open ball in B covers p, but its positive radius implies that it covers S[n] for sufficiently large n, contradicting what was proven about S.

Therefore some finite subsequence of B covers U.

The troublesome part is to show that this can be encoded into ACA. I will assume you can figure out how to encode a real as a set of naturals, and arithmetic on reals as 2-set-parameter sentences over ACA. And also a sequence of sets can be encoded as a single set. Then an open ball is simply a pair of reals representing its centre and radius. A sequence of open balls can hence be encoded as a single set (and we can decode it using parametrized sentences too).

Based on this it is easy to state "there is a finite subsequence of B that covers S[n]", as used in the proof. The recursive construction is where we need WKL.

@DavidReed: Have a look at my proof and see if you get it. =)

David Reed

16:35

@user21820 The version Im interested in is that a subset of R^n is compact iff it is closed and bounded. Or even just the one sided implication that closed and bounded implies compact

user21820

@DavidReed As I have explained, you must choose a version that can be stated in ACA, otherwise it is meaningless to ask whether ACA can prove it.

This is an issue whenever discussing a mathematical theorem in ZFC from a reverse mathematics viewpoint. Different variants that are equivalent to it over ZFC may have different strength over a weak subsystem of second-order arithmetic, if they can be stated at all.

David Reed

Ah. You are referring to the uncountable part? I'm on my phone. I'll reply more when I get to a computer. I don't know much about ACA other than you said once that it is sufficient for most of real analysis.

user21820

Ah I see. Sure. I've to go off now, so I'll see you the next time. In the meantime, you can take a look at the version I've proven, which is for a countable sequence. ACA (as described here) can only talk about natural numbers and sets of natural numbers, and can only construct sets defined by an arithmetical property, and has the full induction schema for all sentences over ACA.

If you really want the full version for any (possibly uncountable) collection of open balls, I think the first note can be proven in predicative third-order arithmetic (ACA is predicative second-order arithmetic), and then the rest follows. If you want for any collection of open sets, then you can first prove a reduction from open sets to open balls again using the density of rationals, I think.

@DavidReed: Ok see you next time!

David Reed

23:44

@Secret Hey there. Do you know if there's any atomic model or theory that predicts the general form of kinetic rate law's? In particular that the rate is proportional to the product of powers of the reactant concentrations? I mean this in a way analogous to how kinetic molecular theory predicts the ideal gas law.

Transcript for

♦ $Mathematics$ Logic

Transcript for

♦ Logic

♦ $Mathematics$ Logic