- This topic has 116 replies, 1 voice, and was last updated 7 months, 3 weeks ago by
.
-
Posts
-
-
What axioms do you believe in?
-
>believe
I dont, I just look at the consequences-
If you believe anything at all, then you must believe some mathematical axioms. You only understand the world through ideas, which are almost identical (though not exactly) to sets.
In other words, If you accept a certain species of animal exists, then you are already implicitly accepting the axiom of pairing, for example. Because the only way to accept it is to conceive animals as an idea in the bigger picture of ideas.
-
sets dont exist in this universe so no
-
yeah but ideas exist and thats what sets are referring to
-
>ideas exist
prove it-
Proof is an idea
-
Not if you write it down with chalk on a blackboard
Then it becomes reality-
yeah but the symbols are not ideas, symbols merely refer to ideas.
-
Which are not real
-
-
-
-
>prove it
everything in the material world is only thought through an idea, that is why language and mathematics is identical with being. Therefore, ideas must be real to. -
You.
I.
-
-
-
-
>pretending all sets behave like finite sets
-
I believe that the the axioms of euclidean geometry will produce good models of some real life situations and that the axioms of spherical geometry will produce good models of some other real life situations.
I don’t believe in one set of axioms more than the other even though they have contradictory axioms.
I don’t know what you mean by believing an axiom.
-
>I don’t believe in one set of axioms more than the other even though they have contradictory axioms.
the fact that you can even distinguish between two different theories implies that you already believe the axioms of extension, ie two sets are not identical if their components are not identical.Whether you locate these principles in mathematics or in a deeper metaphysical reality, you do believe these things because they mediate your action in the world and the comprehension of lower concepts.
-
Read "Believing the Axioms" by Penelope Maddy.
-
I read it once. Didn’t felt too interesting. What is good about the text in your opinion?
https://i.imgur.com/nuaAbvb.gif
For me, its the field axioms. Its all I need for my work.
?
https://en.wikipedia.org/wiki/Tarski%27s_axiomatization_of_the_reals-
Answering your query
>I don’t know what you mean by believing an axiom.
-
-
-
-
Not him but I don’t believe anything at all. I’m paranoid that one day I’m going to punch 2+2 into the calculator and it will equal 3 or 0 or some shit. I can’t do arithmetic without punching into a calc 3 or 4 times and looking at it again and again, if I do an arithmetic problem without triplechecking I get increasing paranoia bording on hysteria.
-
-
FPBP. The only rule in mathematics is consistency from A to B.
-
exactly
[math]2+2=5 implies 4+4=10[/math]-
2+2=5 => you’re a scrotebrained scrote
-
Only if you accept Explosion.
Not necessary for the arithmetic claim above. -
-
-
-
>The only rule in mathematics is consistency from A to B.
scrotebrain. That’s not even a rule.
-
-
-
You mean as in postulations? Well, I’d argue I’m the ubermensch.
-
-
that OP is a scrote
-
Separation
Union
Powerset
Collection
InfinitySimple as.
-
When are two sets equal.
(Question not meant cynically)>Powerset
Unnecessary.-
>Unnecessary.
How so-
Well you can find more conservative claims that give you just as much.
In math you usually don’t need to assume that big sets, even relatively small things as the reals, form a set (you can just deal with the class of all such numbers and express essentially all interesting theorems).On a more unrelated note, this quote is wild
https://en.wikipedia.org/wiki/Elementary_function_arithmetic#Friedman’s_grand_conjectureMaybe for classical topology you actually need some of those strong axioms.
-
-
-
-
Martin-Löf Type Theory + one impredicative universe + induction-recursion. What else?
-
Lambda calculus is an underrated axiomatic system. It has fewer, simpler and more concrete rules than Set theory and properly defines what is valid formula/procedure/method. The theory is woke af upon the idea of substitution. Booleans,naturals,rationals,lists,sets,addition, multiplication and many more can be defined using Church encodings
-
Typing the lambda calculus yields an inconsistent system.
-
-
that reality isn’t a hallucination of my ego
that empiricism and the scientific method are the only way to discover truths about the reality we live in. -
Axiom of infinity is absolutely scrotebrained and the fact that it doesn’t bother most people in the field makes me physically sick.
The rest is fine.-
>Axiom of infinity is absolutely scrotebrained and the fact that it doesn’t bother most people in the field makes me physically sick.
See pic related.-
roasties are braindead and always follow the trend
cantor created crappy maths
-
-
-
Only the ones required for Lain Point Theory.
-
A real number is a cut in the real number line.
-
Sad that not every cut can be pinpointed geometrically.
-
why? can’t you just start from zero and go any direction? what causes the inaccuracy?
-
-
-
-
RCA_0 is all you need. In fact, it’s all you want.
(Possible sans LEM. I don’t know if there’s any serious repercussion from dropping LEM in RCA_0. Likely not.)https://en.wikipedia.org/wiki/Reverse_mathematics#The_base_system_RCA0
-
The reverse math page btw. has a list of what classical arithmetic with only Sigma_1 induction and second order Sigma_1cup Pi_1 comprehension (computable sets) give you, pic related.
Admittedly it’s not all of math, but it’s still hella strong for a theory that isn’t a set theory (and the models of e.g. the reals aren’t super pretty in either)
-
-
You know, I don’t really know what axioms I believe in. But I can tell you what I don’t believe in. The natural numbers. You see, I don’t believe in the axiom of induction… Captcha: YT00D.
-
1 is a natural number
If n is a natural number then n+1 is a natural numberIf a statement is true for every natural number n then the same statement is true for 1 and n+1.(axiom of induction)
I believe that this axiom is valid by proof of contradiction.
If a statement is true for any natural number n but not for n+1 we would have a contradiction since n+1 is any natural number as well. It’s like saying that if a statement is true for any natural n it is also false for any natural k. It doesn’t make sense for induction not to work
-
>If a statement is true for every natural number n then the same statement is true for 1 and n+1.(axiom of induction)
That’s not Induction.
In Induction, the universally quantified claim for the unary predicate is the conclusion (consequent), not the assumption (antecedent).Induction is rejected in the work of predicative arithmetic of
https://en.wikipedia.org/wiki/Edward_Nelson
(The reasoning being that PA "defines" natural numbers by it’s axioms, and so, roughly, his case is that then those axioms shouldn’t have "for all numbers" in them already – lest you’re, in a very nitpicky way – circular)That said, I’m
RCA_0 is all you need. In fact, it’s all you want.
(Possible sans LEM. I don’t know if there’s any serious repercussion from dropping LEM in RCA_0. Likely not.)https://en.wikipedia.org/wiki/Reverse_mathematics#The_base_system_RCA0
and I personally think that at least for [math]Sigma_1[/math]-formulas in the arithmetical hierarchy, Induction should be fine.
Those are the predicates which only have at most one unbound quantifier, namely 1 [math]exists[/math] upfront. E.g. the subset
[math]{nin{mathbb N}mid exists k. (n=2cdot k)}[/math]is [math]Sigma_1[/math]-definable. For any n, know that you can at least (iff it’s actually even) computationally certify membership via giving a k. This example in fact collapses to [math]Sigma_0[/math] if you accept the mod functions as a total function symbol, since then the set is extensionally the same as
[math]{nin{mathbb N}mid (n % 2) = 0}[/math]The [math]Sigma_1capPi_1[/math] formulas are exactly those which a Turing machine can compute. Since those certify both membership and non-membership.
https://en.wikipedia.org/wiki/Certificate_(complexity)
And all the [math]Sigma_1[/math] (certifying membership) ones are at least semi-decidable.
Given the structure of induction, I think it’s fine to adopt induction for those formulas with one existential quantifier.Here’s a listing for schemata of that axiom
https://en.wikipedia.org/wiki/Induction,_bounding_and_least_number_principles
-
>(The reasoning being that PA "defines" natural numbers by it’s axioms, and so, roughly, his case is that then those axioms shouldn’t have "for all numbers" in them already – lest you’re, in a very nitpicky way – circular)
That doesn’t make sense. PA is not the definition of the natural numbers, we already know by Godel and others that PA is not enough to define them. The actual definition is that
– 0 is a natural number
– if x is a natural number, so is SX
– only natural numbers are those resulting from a repeated application of the above two points
It doesn’t refer to PA at all. In light of this, induction is valid for all formulas, not just quantifier-free ones.
>hat said, I’mRCA_0 is all you need. In fact, it’s all you want.
(Possible sans LEM. I don’t know if there’s any serious repercussion from dropping LEM in RCA_0. Likely not.)https://en.wikipedia.org/wiki/Reverse_mathematics#The_base_system_RCA0 and I personally think that at least for Σ1-formulas in the arithmetical hierarchy, Induction should be fine.
Why wouldn’t it be fine for all formulas? And you mean both Sigma_1 and Pi_1 formulas correct?-
First off, I’m not defending Nelsons view.
As for your argument, you say
>only natural numbers are those resulting from a repeated application of the above two pointsBut if you drop induction IND from PA, i.e. look at Robinson arithmetic (which actually adds some stength of IND back), then that theory already has models with "infinite natural numbers at the end". It’s shortly described at the bottom here
https://ncatlab.org/nlab/show/Robinson+arithmeticThe statement you wrote down can, as far as formal theory concerned, only be held if you also consider induction.
>Why wouldn’t it be fine for all formulas?
Just seems like too strong an assumption and extra assumptions can always be stated explicitly (or, in a text, you just state that now you switch to a stronger theory.)>And you mean both Sigma_1 and Pi_1 formulas correct?
I just meant to require Sigma_1 induction, but I think depending on the rest of the context you get both of those sides for induction in particular-
>The statement you wrote down can, as far as formal theory concerned, only be held if you also consider induction.
My point is that it’s a separate definition independent of induction. I’m not referring to any formal system, not PA, not ZFC, not Q not anything else to define the natural numbers. After you do so, you should see why induction for ALL formulas is true, and that there’s no circularity.
Of course
>only natural numbers are those resulting from a repeated application of the above two points
cannot be formulated in first order logic, but I’m not trying to. Definitions don’t all have to be formulated in a strict formal system.
>Just seems like too strong an assumption and extra assumptions can always be stated explicitly (or, in a text, you just state that now you switch to a stronger theory.)
Too strong? Too strong for what? What matters is that it’s true, so you use it to make your job easier. Unless you also want to consider nonstandard models where induction for more complicated formulas fails, but nobody cares about that.
>I just meant to require Sigma_1 induction, but I think depending on the rest of the context you get both of those sides for induction in particular
Is there any reason to prefer Sigma_1 formulas to Pi_1? To me they seem two sides of the same coin.-
>Definitions don’t all have to be formulated in a strict formal system.
You do you, I’m not gonna argue you should be more concise with your background if you don’t like>Too strong? Too strong for what?
Too strong as in including subsets of N which we don’t even know are decidable. Again, I’m not pushing this conservatism on anyone, so I’m not gonna argue more for that>To me they seem two sides of the same coin.
Yeah pretty much. I think in complexity theory the Sigma side is the more "positive" phrasing, namely unbounded search without giving a time bound, but with certainty that till you certainly find something for the positive cases. (E.g. you can dovetail algorithms and computably generate the subset of N defined as all the numbers for which the "3x+1" collatz function applications eventually end in 1. Those searches will give us all such numbers even if it may be the case that there’s counter-examples, or uncomputable n’s.)I think historically Sigma_1 and the induction principle for it is just where computability theorists and complexity theorists see the theory diverge into the less computable realm / oracles / set theory like comprehension.
As opposed to the pic in
The reverse math page btw. has a list of what classical arithmetic with only Sigma_1 induction and second order Sigma_1cup Pi_1 comprehension (computable sets) give you, pic related.
Admittedly it’s not all of math, but it’s still hella strong for a theory that isn’t a set theory (and the models of e.g. the reals aren’t super pretty in either)
, pic related is what you get if you adopt some weak choice ("for every infinitely big tree there exists an infinite path").
Clearly this has some important mathy theorems, so it’s not like you should stop at RCA0. But you can be explicit about your assumptions beyond it too.Or you just adopt ZFC, I don’t care, do what you want. I’m off for today.
-
-
-
-
-
>I believe that this axiom is valid by proof of contradiction.
>This axiom
>Valid by proof-
I could have worded it better, I agree. I see it more like a logical consequence rather than a rule
-
-
-
-
OP is always a scrote.
-
Maybe said differently, if you adopt induction only for [math]Sigma_1[/math]-predicates [math]exists k. P(n, k)[/math], where [math]P[/math] only contains computable operations,
then via induction you enable yourself to prove statements
[math]forall n. exists k. P(n, k)[/math]
for which you know that indeed you can, for each k, computably certify why [math]P(n, k_n)[/math] holds.If you adopt induction for predicates in n with longer chains of quantifiers, then the axiom itself is what proves them.
-
Are there any arithmetic statements that you can prove using induction only for Sigma_1 and Pi_1 predicates but cannot prove using induction only for Sigma_1 predicates?
-
No, over Robinson arithmetic (PA with induction removed but the [math]Sigma_1[/math] claim added back that each nonzero number has a predecessor), the induction schemas on level n are equivalent, i.e.
[math]Qvdash {mathsf {ISigma_n}} iff {mathsf {IPi_n}}[/math]which are the names for Q+the n level induction.
Of course, this is something "I knew" but in reality only knew from Mathoverflow and the bottom of this Wikipedia page
https://en.wikipedia.org/wiki/Induction,_bounding_and_least_number_principles#Relations_between_the_principlesSo I dug up the reference and downloaded this 1978 Springer book with the paper, pic related. (The proofs are quite concise there, but basically clearly seem to imply that you can switch out the outer quantifiers and do the translation explicitly)
-
What is a in the proof? Free variable or actual numeral? If free variable i dont get why we suppose not theta(a), rather than not for all a, theta(a) or there exists a s.t. theta(a).
-
Again, I find those proofs far to concise if you’re not in the field, and so hard to read.
That said, I think what he tries to say is the following:
Sidenote: Induction reads
[math]Big(theta(0) land forall(x:N). big(theta(x)totheta(x+1)big)Big)to forall (y:N). theta(y)[/math]Then the first paragraph, with a bunch of verbosity filled in by me, would read:
"Let [math]theta[/math] be a unary predicate over the numbers of either Sigma or Pi type. Suppose
[math]theta(0) land forall(x:N). big( theta(x) to theta(x+1) big) [/math]
but
[math]negforall (y:N). theta(y)[/math],
i.e. but
[math]exists (z:N).neg theta(z)[/math],
i.e.
[math]neg theta(a)[/math]
for some particular [math]a:N[/math],
i.e. assume the consequent in Induction is wrong despite the antecedent being validated.
Then note that we can also form those two predicates in y for which Induction fails as well
(…)"-
The thing that confuses me is that we’re working at the level of formal logic, and not theta(a) seems to imply that we have an actual witness for not for all x, theta(x), but I see no reason for this to be the case. At the level of formal logic, there’s no reason to expect to have a witness just from the statement not for all x, theta(x).
Perhaps he meant to say [math]exists a neg theta(a)[/math], in which case the statement [math]exists w (a = y+w land neg theta(w) ) [/math] really is
[math]exists w exists a(neg theta(a) land a = y+w land neg theta(w) )[/math], which then through coding three variables at once can be transformed into a [math] Sigma_n[/math] statement as required. For the other statement I guess we want to use [math]forall a[/math] and add a condition which takes a to be the smallest one to single it out.
Perhaps for you it’s trivial but for someone like me with not much experience it’s far from trivial.
Do you think that’s what we meant?
And then induction fails because inductive hypotheses (2 of them) are true and the forall statement is false. And it’s false by taking y= any of the a’s satisfying that property because then w is forced to be zero and it would assert [math]neg theta(0)[/math] which we know is false. Did I get that right?-
¬∀(n:N). θ(n)
to
∃(n:N). ¬θ(n)
is classically, a stronger form of the Markov rule
Using this to instantiate an
a, with ¬θ(a)
is a natural deduction rule too.https://en.wikipedia.org/wiki/Markov%27s_principle#In_Intuitionistic_logic
https://en.wikipedia.org/wiki/Existential_instantiationI don’t want to go through the pains of interpreting a super short 70’s typewritten book, I’d want to read a more common text – I think those papers and books aren’t so much concerned with foundations than with complexity theory
-
>Using this to instantiate an
>a, with ¬θ(a)
>is a natural deduction rule too.
What is it called? Do you have a link to the rule? As I understand, here a is neither a free nor bound variable, but some other kind of variable?-
I literally linked it, wtf
-
Oh, didnt notice the second link, thanks
-
So without this rule of inference and using Markov rule can you also form a proof along the lines I indicated?
-
As I said a couple of times, I’m not really interested in taking it apart. Interpret that as "I donno."
I’ve never seen a theory without that rule of inference, though ∃. It’s even more viable if you don’t have LEM.
I’d think you need a Markov rule, which imho one should adopt for the lower levels of the hierarchy. (Sidenote: Brower’s school of constructivism can’t accept Markov’s rule for consistency reasons, but Markov’s school of course does.) -
I’m mainly interested in classical logic here.
-
Under Curry Howard, if you’ve proven
[math]exists u. P(u)[/math],
then this literally means you got a pair [math](u, p)[/math], that typechecks as
[math](a, p_a) colon exists u. P(u)[/math],
where p witnesses [math]P(a)[/math], and so typechecks as
[math]p_a colon P(a)[/math]So the left projection of any proof of [math]exists u. P(u)[/math] literally is the [math]a[/math] where’s looking for and that’s what the rule more abstractly allows you to do.
tl;dr if you have proven an existential statement constructively, then you got that witnessing a anyway, so the rule is a sort of real life tautology in that context.Of course classically the rule is somewhat of a meme, as ZFC will e.g. proof the existence of choice functions that provably can’t be defined.
It proves
[math]exists f. text{f is a choice function for this and that}[math]
but actually there’s no term g that does the job.
The rule is okay still, I suppose, insofar as that "term a" is only used during a proof and doesn’t have to linger around after. -
Not if you interpret [math]exists[/math] as the squashed variant of the existential type, or the one in Prop if you were in CIC. In general, this type does not enjoy choice.
If you extend your theory with classical logic in propositions it then makes perfect sense because there are no such choice functions in general but it’s fine to merely accept their existence.
-
>I’ve never seen a theory without that rule of inference, though ∃.
You’ve never heard of LK and LJ? -
I wouldn’t know by heart which rules those fulfill
-
-
-
-
-
-
-
-
-
-
for each n,
-
>Assume a proper class of Woodin cardinals exists
-
for what purpose?
-
Can you turn down the bass?
-
-
The one that tells us we’re bonked and can’t really know everything anyways.
-
The axiom of choice, but ONLY the axiom of choice.
-
woke af
-
For me, it’s global choice.
-
-
Praxeological axioms.
-
Woke af
-
-
Axiom 1: Inconsistency is allowed wherever I deem necessary.
-
Woke af schizo tyrant
-
This meme or any of its variations have never been funny. You’re a low IQ scrote and I hate you.
-
You’re the scrote scrote for assuming it was meant to be funny. Please suffocate.
-
What is it meant to do if not be funny?
-
It’s schizo logic for the schizo. Go die now.
-
-
-
-
-
-
[math]exists f. text{f is a choice function for this and that}[/math]
-
https://i.imgur.com/nuaAbvb.gif
For me, its the field axioms. Its all I need for my work.
-
Your work must be very boring then. There’s very little you can do with just the field axioms.
-
-
My math, my choice.
-
Falso, the patrician choice.
https://inutile.club/estatis/falso/ -
You cannot trust axioms. Any axiom is true in the theory for which it is an axiom.
But it is likely to be wrong for other theories.
Example: the theory for spiders says as an axiom that each animal has eight legs.
But an ostrich has two legs, which is fewer than eight. hence the axiom is wrong and
it cannot be trusted.-
>You cannot trust axioms. Any axiom is true in the theory for which it is an axiom.
The second sentence exactly says that it’s not a matter of "trust", but choice>Example
Convoluted way of saying that "theory" and "axioms" always go together and axiom sets don’t mix among each other.-
A sane person of course agrees with you.
But how else explain the concept of axioms to Wildberger and his followers?-
He’s an old old man, he gets a free pass from me.
-
you think wildberger doesn’t understand the concept of axioms?
-
Stop replying to scrotebrains.
-
-
>Wildberger and his followers
They’re all just LARPers anon, no one is stupid enough to reject the notion of real numbers.
-
-
-
-
What does ZFC taste like?
-
ZFC + Con(ZFC) + Con(ZFC + Con(ZFC)) + Con(ZFC + Con(ZFC) + Con(ZFC + Con(ZFC))) +…
to believe otherwise is sheer lunacy
-
What about Con(ZFC + Con(ZFC) + Con(ZFC + Con(ZFC)) + Con(ZFC + Con(ZFC) + Con(ZFC + Con(ZFC))) +…)?
-
You still can’t prove it’s consistent, you’d need to add transfinite towers of consistency. And then starts the problem of the kind of ordinals you believe in.
-
>You still can’t prove it’s consistent
Make it an axiom.
-
-
-
-
Why do they always say that NBG is bad?
-
-
Thanks, I more or less know what NBG is.
So this Halmos "No Bloody Good" is just a joke?
-
-
-
All of them.
-
I believe that a line is an interval between two points that can be extended indefinitely in either direction.
-
go on…
-
-
Transitive Closure OR Countable Choice, but not both
-
>OR
>but not both
That’s called XOR. -
Why?
Also, isn’t countable choice vastly milder than transitive closure for all sets?
-
-
BUMP
-
a point on a line is a point on a line.
so far in X years of this shit, no one has managed to express a dissenting opinion that makes any sense
-
- You must be logged in to reply to this topic.