« first day (612 days earlier)      last day (2205 days later) » 

Leaky Nun
Leaky Nun
12:19 AM
ok
 
 
6 hours later…
user21820
user21820
6:11 AM
Sorry typo above. It should be subclass in func(ptype,separable). and that would allow us to write minfounded equivalently:
minfounded = ( separable S −> { linorder(S) < : forall T in subclass(S) ( exists x in S ( x in T ) implies exists m in T forall x in T ( x<m implies not P(x) ) ) } ).
This version is closer to the conventional "every non-empty subset has a minimum", but note that it only works for subclasses of S, and not arbitrary subtypes of S.
I forgot to say that { S x : P(x) } is short-hand for { x : x in S ?and P(x) }.
 
Leaky Nun
Leaky Nun
ok
 
user21820
user21820
6:28 AM
@LeakyNun: So what's your precise definition of accessible?
 
Leaky Nun
Leaky Nun
6:44 AM
@user21820 I thought we already defined it
23 hours ago, by Leaky Nun
to show that x is accessible, you show that everything less than x is accessible
inductive definition
if you're still not satisfied, define it as the smallest subset A such that ∀x[(∀y(y<x→y∈A))→x∈A]
existence guaranteed by Knaster Tarski
 
user21820
user21820
@LeakyNun This is much clearer. I was just writing out 3 possible interpretations of your quote, 1 of which was this.
 
Leaky Nun
Leaky Nun
i'm interested
 
user21820
user21820
Well your quote basically stated "forall x in S ( forall y in S ( y<x implies acc(y) ) implies acc(x) )", but that could mean either that you claim such a property acc exists, which is not claiming anything because you could have acc(x) for every x in S, or you claim that it works for all properties acc, which is then the same as "S is progressive". Or it is what you said.
 
Leaky Nun
Leaky Nun
hmm, the powerset happens to be a fixed point
and there goes the equivalence between inductive definitions and indexing by natural numbers
this inductive definition goes to transfinite
 
user21820
user21820
You said least fixed point, so it's no issue that there are other fixed points. But there is another issue.
 
Leaky Nun
Leaky Nun
6:53 AM
which is
 
user21820
user21820
If a total-ordering is called a well-ordering iff every element is accessible, then isn't that equivalent to progressive?
Then I don't get what's so good about using "accessible" in constructive mathematics, since it is 'more' impredicative.
 
Leaky Nun
Leaky Nun
but you quantified over all sets
it's only "more" impredicative because we used Knaster Tarski to justify induction
I would rather take induction as an axiom
 
user21820
user21820
Firstly, I didn't quantify over all sets, but only over func(S,bool), which could be re-interpreted as just saying that we can prove progressivity where P is just a predicate-symbol. This is why it's practically 100% predicative because we are essentially using nothing more than logic.
 
Leaky Nun
Leaky Nun
> 100% predicative because we are essentially using nothing more than logic
 
user21820
user21820
It is true that to prove equivalence of progressivity and accessibility requires interpreting the function types internally. But if we don't want to prove the equivalence we can stick to the symbolic interpretation I just stated.
 
Leaky Nun
Leaky Nun
6:58 AM
this is 100% wrong
 
user21820
user21820
@LeakyNun I said "practically 100%", not "100%". And I meant first-order logic there.
 
Leaky Nun
Leaky Nun
did you
 
user21820
user21820
Yea I didn't edit that message. =P
Anyway. I haven't finished.
Secondly, Knaster Tarski can either be proven impredicatively (as you know) and this proof involves instantiating an impredicatively defined object. This makes it different from the apparent impredicativity in progressivity since that instantiated object has to actually exist in the intended interpretation. It also can be proven by transfinite induction, but that means that it will only be predicative up to the ordinals that you believe are predicative, which may be very tiny?
But I understand that some people think that inductive definitions are self-justifiable... I think it's fine as long as one does not presume that the inductive definition constructs a minimal instance satisfying it, otherwise we are essentially appealing to the fixed-point theorem.
You may like the idea behind ATR, which allows you to construct any set in second-order arithmetic that represents a sequence of sets defined by a recursion along any well-ordering (on N). So you can bootstrap quite high by repeatedly constructing new well-orderings using previous ones.
 
Leaky Nun
Leaky Nun
who is ATR?
 
user21820
user21820
7:18 AM
@LeakyNun It's the last subsystem of second-order arithmetic that a significant fraction of logicians accept as predicative.
Reverse mathematics
Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in contrast to the ordinary mathematical practice of deriving theorems from axioms. It can be conceptualized as sculpting out necessary conditions from sufficient ones. The reverse mathematics program was foreshadowed by results in set theory such as the classical theorem that the axiom of choice and Zorn's lemma are equivalent over ZF set theory. The goal of reverse...
ACA allows you to construct any finite Turing jump, but that's its limit. ATR easily allows you to iterate the jump operator along any well-ordering.
 
Leaky Nun
Leaky Nun
ZFC is a first order theory #changemymind
 
user21820
user21820
@LeakyNun Does it mean you now think it is first-order or you don't?
 
Leaky Nun
Leaky Nun
it means it is technically a first order theory
 
user21820
user21820
Yes it is.
Historically though, it was based on an idea that turned out to be logically problematic, namely set = set→bool. The schemas are only expressed as schemas to fit into the first-order logic paradigm. A lot of set theorists still think of them as expressing second-order notions, even though they clearly can't.
@LeakyNun: And hence, a lot of set theorists like to work in MK instead of ZFC, which is literally a full second-order extension of ZFC in the same way Z2 is a full second-order extension of PA.
Morse–Kelley set theory
In the foundation of mathematics, Morse–Kelley set theory (MK), Kelley–Morse set theory (KM), Morse–Tarski set theory (MT), Quine–Morse set theory (QM) or the system of Quine and Morse is a first order axiomatic set theory that is closely related to von Neumann–Bernays–Gödel set theory (NBG). While von Neumann–Bernays–Gödel set theory restricts the bound variables in the schematic formula appearing in the axiom schema of Class Comprehension to range over sets alone, Morse–Kelley set theory allows these bound variables to range over proper classes as well as sets, as first suggested by Quine in...
 
 
1 hour later…
user21820
user21820
8:54 AM
@user21820 This is related to something I just found: golem.ph.utexas.edu/category/2012/10/…. Unfortunately, on that thread there is no comment along the lines of my post. My response (which I can't submit there) is as follows:
> It is easy to prove with absolutely no order theory that for infinite X, if X×X bijects with X then P(X)×P(X) bijects with P(X). (Hint: Let c in X. For any set S, let S' = { (0,a) : a in S } union {(1,c)}. Use an injection from X×X into X to get an injection from X' into X, and then get an injection from X'×X' into X, and then consider f : P(X)×P(X) -> P(X) where f(S,T) = { f(a,b) : a in S' and b in T' }.) Also, #(N×N) = #(N) is arguably a number-theoretic fact. These together imply that every set we need in 'ordinary' mathematics would satisfy the desired theorem, without any order theor…
 
 
3 hours later…
user21820
user21820
11:31 AM
 
famesyasd
famesyasd
@user21820 yeah, I would like to continue somewhere if you don't mind it...
 
user21820
user21820
11:53 AM
This is amusing (and makes me wonder what happens in my type theory):
3
A: Results in cardinal arithmetic

Noah SchweberA lot of modern set theory has roughly had the theme, "Nothing about cardinal arithmetic can be proved in ZFC." My favorite source of counterexamples to this idea is PCF (possible cofinalities) theory. This was invented by Shelah, and used by him and others to prove a number of ZFC-results; see ...

 

« first day (612 days earlier)      last day (2205 days later) »