[ 3 / biz / cgl / ck / diy / fa / ic / jp / lit / sci / vr / vt ] [ index / top / reports ] [ become a patron ] [ status ]
2023-11: Warosu is now out of extended maintenance.

/sci/ - Science & Math


View post   

File: 29 KB, 343x450, Leopold_Kronecker_1865.jpg [View same] [iqdb] [saucenao] [google]
15803575 No.15803575 [Reply] [Original]

mandatory /sci/ finitism set theory debate

>> No.15803625

How do finitists integrate the area under a curve?

>> No.15803641

>>15803625
Finitists don't reject infinity, just infinite objects (broad stroke explanation). Analysis is still possible under a finitist school of thought.

>> No.15803959

>>15803575
The idea of infinity in math is to talk reliably about finite objects (it is true that any real world object is finite after all), using infinite objects described by axioms that we hope they aren't contradictory when assumed together. While the non-contradiction cannot be formally established (unless the system is actually inconsistent), the usual math systems (set theory, type theory, arithmetic) hadn't been found to be inconsistent so far.
There are many conservativity results from proof theory that guarantee that many extra axioms that seem to add speculation in math are atually hamless, for instance:
1°) We recall that in arithmetic, the halt of a specific Turing machine can always be expressed by a formula of the form "forall x, exists y, R(x,y)" where every quantifier inside R is bounded. There is a theorem from Harvey Friedman which say that if such a formula is proven in Peano arithmetic, then it has also a proof in intuitionistic Heyting arithmetic (Peano without the rule of excluded middle). The fact is established by translating the proof using first Gödel double negation traduction and then Friedman's translation (the complexity of the transformation is low, no exponential explosion iirc). So there is no reason to whine about "non constructive excluded middle" for such sentences (about concrete objects).
2°) In set theory, let V_(omega) the first element of the Von Neumann hierarchy indexed by an infinite ordinal. V_{omega} is made up of all finite combinatoric objects, including numbers. Let P be a formula in which every quantifier is bounded by V_{omega}. Then if there is a proof of P within ZF + AF + "V=L" (AF is the foundation axiom and V=L is Gödel constructibility axiom which yields the axiom of choice "AC" and the generalized continuum hypothesis). Then P is provable in ZF alone (see Krivine set theory), in particular without the axiom of choice. So when talking about finistic objects, using or not AC doesn't change anything.

>> No.15804279

>>15803641
We first properly define integration, area and curve. After that it becomes trivial.
By the way, a lot of calculus can be interpreted in a finitist way. The actually useful parts of calculus, anyway. Read Bishop's constructive analysis.

>> No.15804283

>>15804279
Constructivism is not the same thing as finitism. I ain't afraid of no function.

>> No.15804295

>>15803959
>The idea of infinity in math is to talk reliably about finite objects (it is true that any real world object is finite after all), using infinite objects described by axioms that we hope they aren't contradictory when assumed together
This is wrong on many counts. You can talk about finite objects reliably without using infinity. Infinity is used to, surprise surprise, talk about infinite objects.
It also hasn't been demonstrated that any real world object is finite. That's just an assumption of yours that is irrelevant for mathematics. Mathematics deals with abstract objects, not physical (or as you refer to them, real world) ones. Whether or not there existed infinite objects in the physical universe (whatever that means) wouldn't change the fact that finitism is objectively the only rigorous approach to mathematics.
>While the non-contradiction cannot be formally established (unless the system is actually inconsistent), the usual math systems (set theory, type theory, arithmetic) hadn't been found to be inconsistent so far.
This is absolutely wrong. Many set theories have been demonstrated to be inconsistent time and time again. Look up russel's paradox, burali-forti paradox, Kunen's inconsistency theorem. What mathematicians/set theorists do then is to patch it up and claim that now it's ok. There has been no effort to come up with a good set theory from first principles, with proper justification for why it can't fail like the previous failed set theories. What we're working right now is set theory v0.1.3 and hoping the next bug won't be too disastrous.
Meanwhile, finitism is about being rigorous from the start. That's why finitist systems haven't been proven inconsistent, in fact they have been proven to be consistent many times.

>> No.15804297

>>15804283
Finitists are ok with functions as finite objects.

>> No.15804310

>>15803959
>1°) We recall that in arithmetic, the halt of a specific Turing machine can always be expressed by a formula of the form "forall x, exists y, R(x,y)" where every quantifier inside R is bounded. There is a theorem from Harvey Friedman which say that if such a formula is proven in Peano arithmetic, then it has also a proof in intuitionistic Heyting arithmetic (Peano without the rule of excluded middle). The fact is established by translating the proof using first Gödel double negation traduction and then Friedman's translation (the complexity of the transformation is low, no exponential explosion iirc). So there is no reason to whine about "non constructive excluded middle" for such sentences (about concrete objects).
Not a big surprise as PA is finitist and rigorous as far as I'm concerned. I am open to be challenged.
> ZF + AF + "V=L" (AF is the foundation axiom
Foundation is included in ZF.
Also your second point is just saying one schizophrenic nonsensical system can in some cases prove the same things as another nonsensical schizophrenic system. Doesn't say much about finitism.

>> No.15804312

Finitists are m-zombies

>> No.15804320

>The source of this incoherence is obviously the fact that axiomatic set theory was
developed not in a philosophically principled way, but rather in an opportunistic
attempt to preserve as much naive set theory as possible without admitting any
obvious inconsistencies. This was accomplished by, in effect, adding just enough
constructivity to the naive picture to avoid the standard paradoxes. The result is
a nonsensical jumble of constructive and non-constructive ideas.
https://arxiv.org/pdf/0905.1677.pdf
Set theory is a joke.

>> No.15804326

>>15804295
>Russell's paradox
This is where I realized you have no idea what you're talking about.

>> No.15804336

>>15804326
> never heard of Frege's basic law V

>> No.15804340

>>15804295
>This is absolutely wrong. Many set theories have been demonstrated to be inconsistent time and time again. Look up russel's paradox, burali-forti paradox, Kunen's inconsistency theorem.
The most usual systems haven't been found inconsistent. Kunen only debunk some large cardinal axioms. ZF have never been found out to be inconsistent.
>It also hasn't been demonstrated that any real world object is finite. That's just an assumption of yours that is irrelevant for mathematics.
I haven't said that. Plus in maths assumptions aren't beliefs but just a list of what would need to be debunked if a theorem was found to be wrong.
>>15804310
>Not a big surprise as PA is finitist
PA is not finitist; neither are its most popular fragments (the one from reverse mathematics: RCA0, WKL0) etc (and these are subjected to the second Gödel theorem and could be inconsistent too); in fact even Robinson arithmetics "Q" is not finistist? Why? because none of these theories have a finite model. You could talk about objects that have no counterpart in the real world like 100^1000 (although Q cannot define powers, it is not hard to write 1000 followed by 999 times "x 100 " in a couple pages of a pdf file ); although such a number doesn't describe any physical process and you would be in trouble if you had to prove it is even (induction, where are you ?)...
Finitism is mostly a meme imho

>> No.15804352

>>15804340
>The most usual systems haven't been found inconsistent
The first set theories have been repeatedly found to be inconsistent.
> Kunen only debunk some large cardinal axioms
Large cardinal axioms give rise to different set theories.
> ZF have never been found out to be inconsistent.
Neither has "ZF + riemann hypothesis" or "ZF + not riemann hypothesis". This is not evidence that either is consistent.
If you think ZF is consistent, explain why.
> I haven't said that.
What relevance does the "real world" have to mathematics then?
> PA is not finitist
For me it is. PA with its usual interpretation refers to natural numbers, which are finite objects.
> and these are subjected to the second Gödel theorem and could be inconsistent too
Just because a theory is subjected to the second Godels theorem doesn't mean it could be inconsistent, that's just lazy thinking. It just means that the formal proof of its consistency as formalized within the system itself cannot be carried out within the system itself. Doesn't mean there is no proof of its consistency.
There are several proofs of consistency of PA. I know it is consistent (what's more, it has a model). Not the case with ZFC.
> in fact even Robinson arithmetics "Q" is not finistist? Why? because none of these theories have a finite model
Ok that's just disagreeing over definitions of finitism. To me, a system is finitist as long as it has interpretation whose domain consists of finite objects (which in principle could be written down on a large piece of paper, and looking at which I could in general tell whether or not it is an object of that type).

>> No.15804362
File: 65 KB, 654x540, Screenshot 2023-10-14 204127.png [View same] [iqdb] [saucenao] [google]
15804362

It's also important to note that it may very well be that ZFC is consistent, but it could still be schizophrenic nonsense that proves false things in arithmetic. In fact, there is no reason to think that it doesn't prove false things in arithmetic.
The question of consistency is only relevant as long as you want to prove correct statements in the first level of arithmetic hierarchy. If you want to be correct about more complicated arithmetic statements, you need much more than consistency: you need arithmetic soundness.

>> No.15804367
File: 52 KB, 850x716, extrapolate.png [View same] [iqdb] [saucenao] [google]
15804367

> we haven't found an inconsistency yet therefore it's consistent and sound

>> No.15804371
File: 850 KB, 1024x1024, 1656874866952.png [View same] [iqdb] [saucenao] [google]
15804371

>> No.15804373
File: 109 KB, 500x394, 1507496185924.png [View same] [iqdb] [saucenao] [google]
15804373

>The point of view on which I disagree with most mathematicians resides in the basic assertion that mathematics and the natural sciences — which have recently been separated by this name from the remaining sciences, the so-called sciences of the mind (Geisteswissenschaften) — must not only be free of contradiction, but must also result from experience and, what is even more essential, must dispose of a criterium by which one can decide, for each particular case, whether the presented concept is to subsume, or not, under the definition. A definition which does not achieve this, can be advocated by philosophers or logicians, but for us mathematicians, it is a bad nominal definition. It is worthless.
- Leopold Kronecker

>> No.15804637
File: 436 KB, 1255x713, 1687121072415090.png [View same] [iqdb] [saucenao] [google]
15804637

>>15803575

>> No.15804638
File: 393 KB, 1241x800, 1680293422868711.png [View same] [iqdb] [saucenao] [google]
15804638

>>15804637
https://odysee.com/@musicam-geometria-utebantur:6/wildberger-edit-v1:4

>> No.15804678

>>15803575
Can you do topos theory in finitism?

>> No.15804688

How do finitists cope with the fact that infinite objects exist

>> No.15804714

>>15804688
>infinite objects exist
Prove it. Or is that simply your theological belief?

>> No.15804722

>>15804371
Infiniteschizos have been real quiet since this dropped...

>> No.15805131

>>15804722
worst than "infiniteschizos", there are the "kronecker/PAschizos" who think they don't talk about infinite objects (when PA does not have any finite models). Just write 7^(7^(7^(7^(7^(7^7))))) on that sheet of paper I dare you. Is its list of digits "real" to you?

>> No.15805144

>>15804320
constructivism is virtue signalling. In COQ theorem prover you have implementation of the Ackermann function A (which is then total in that theory). Let P be a predicate such that P(0) and forall , P(x) -> P(1+x). Then COQ proves A(8,8) where 8:= 1+ (1+ (1+ (1+ (1+ (1+ (1+ 1)))))) (And A satisfies A(0,x) = 1+x, A(1+y, 0) = A(y, 1) and A(1+y,1+x) = A(y, A(1+y, x)) for every integers x,y. You may enjoy finding closed formulas for A(k,n) for every n and every k ranging from 0 to 4 for a good laugh). How much of this is real? Friedman's theorem states that whether you use excluded middle or not, that doesn't change anything about forall-exists- statements (the ones able to state a Turing machine halts).

>> No.15805156

>>15804352
>There are several proofs of consistency of PA. I know it is consistent (what's more, it has a model). Not the case with ZFC.
How do you deal with the fact that Theories which prove the consistency of Peano are in fact stronger (they assume strictly more) theories (like ZFC) and as such, are possibly speculative or irrelevant from your point of view? For the record, The consistency of ZFC is proven by "ZFC+ there exist an inaccessible cardinal", or (it is essentially the same) Bourbaki set theory + there exists Grothendieck universes.
>(what's more, it has a model). Not the case with ZFC.
Consistent theories do have models (the completeness theorem) according to WKL0 which is a conservative extension of I_sigma_1 (arithmetic with the induction schema restricted to forall-exists type formulas), and of course in that case the model is countable. Although WKL0 cannot prove ZFC has a model unless both theories are inconsistent, it still applies.

>> No.15805219

>>15804362
Arithmetic soundness is meaningless. There are no two popular different theories (even fragments of Peano arithmetics) that prove the same sentences about numbers and computer programming (I mean forall/exists in the arithmetical hierarchy), since if such a theory T proves T' is consistent, it proves a certain Turing machine X halts (the one looking aggressively for a proof of 0= 1 in T) while T' cannot (or would be inconsistent). Q doesn't even prove that the algorithm that picks an integer n and return 2^n halts for all entries n. So-called "numbers" only live within theories and none agree on all statements about them. Finitism is really the last refuge of platonism as someone said once.

>> No.15805220

>>15805219
>it proves a certain Turing machine X halts
Sorry I meant "it proves a certain Turing machine X DOES NOT halts" of course.

>> No.15805324

>>15805156
As a finitist, it's not the most important thing for me which theory can a proof be formalized in. First and foremost, the question is whether or not the proof is concinving. This is the original meaning of the word proof, which has been subverted by the formalists who couldn't philosophically justified their own delusions, so decided to debase the meaning of proof and reason.
The fact that natural numbers form a model for PA is enough for me to believe in its consistency (and arithmetic soundness).
From a more formalist viewpoint, Gentzen's proof of consistency of PA using the well-foundedness of the constructive ordinal epsilon_0 I also find thoroughly convincing.
If you don't think either of these proofs are convincing, present reasons why.

>> No.15805327

>>15805219
>Arithmetic soundness is meaningless
You have not demonstrated this.
> There are no two popular different theories (even fragments of Peano arithmetics) that prove the same sentences about numbers and computer programming (I mean forall/exists in the arithmetical hierarchy), since if such a theory T proves T' is consistent
A theory T' can prove the same arithmetic statements as a theory T without proving that T' is consistent.

>> No.15805406

>>15805327
What is an "arithmetical statement?" The soundness of a theory is a sigma_1 statement, namely a couple existential quantifiers followed by a formula written with +,x, 0,1,=, logical connectors and only bounded quantifiers.

>> No.15805415

The universe isn't computable on a turing machine, it requires the contimuum
https://www.youtube.com/watch?v=QPMn7SuiHP8

>> No.15805437

>>15805406
>The soundness of a theory is a sigma_1 statement
Prove it.

>> No.15805443

>>15805437
Mmm I meant: the *inconsistency* of it, my mistake. It is just "there is a number which is a proof of 0=1". But yet T' will prove the negation of suh a statement about T while T could not unless it is inconsistent. ZFC says the function f which take an integer and return 0 if the integer is a poof if "Peano proves 0 = 1" is a constant function, while Peano cannot prove f is constant (unless Peano is inconsistent). Same holds if you replace ZFC by Peano and Peano with let's say RCA0.

>> No.15805458

>>15805443
An arithmetic statement is a Pi^0_n statement for some n.

>> No.15805488

>>15805458
OK but then, since every statement in the language of arithmetics, has a prenex form, it is automatically a P^0_n statement and this incudes te statement I was talking about and that no two different popular theories prove the same (ZFC, Peano, WKL0, Q ...)

>> No.15805493

To me, finitism provides a spiritual comfort the metaphysical safety from reduced risk that my mind would, in a void, get stuck computing things for small eternities.

I don't know enough but my starting point for proper finitist set theory and arithmetic -analogues would maybe be lambda calculus.

Ideal finitist mathemathics would have certain numbers, which then are never exceeded in computations. More rigorously, the structures should have limited size as information. Kolmogorov complexity can be used to define finitism in this sense.

I have made "crude" attempts to define arithmetic where it "wraps" around the maximum allowed positive integer using Galois fields; the recursive processes can still get so large that the information in them exceeds the number.

Functionalism may be a requirement of finitism.

---

Got idea of schemes with limited / finite computational propertirs in the algebraic structures while writing this.

>> No.15805664

>>15804637
>>15804638
中出し

>> No.15806007
File: 161 KB, 768x887, fig_001.jpg [View same] [iqdb] [saucenao] [google]
15806007

>>15805664
>中出し
仙扶桑

>> No.15806154

can finitists make statements that are applicable to all natural numbers

>> No.15806155

>>15806154
Sure! Here's one: all natural numbers are natural numbers.

>> No.15806157

>>15806155
how do the finitists define natural numbers

>> No.15806161

>>15806157
Strings of digits 0-9 like you see in elementary school.

>> No.15806163

>>15806161
why aren't there are infinite of those

>> No.15806165

>>15806163
There are.

>> No.15806168

>>15806165
how is it possible to unify that with infinite objects not existing

>> No.15806171

>>15806168
Natural numbers are not infinite objects.

>> No.15806176

>>15806171
but there are infinite of them
if you say something about all natural numbers
then surely you are quantifying over an infinite number of objects, and we can consider that quantification an infinite object

>> No.15806177

>>15806176
>and we can consider that quantification an infinite object
You can but you don't need to.

>> No.15806185

>>15806177
can finitists do anything infinitists can

>> No.15806186

>>15806176
You can also consider rational numbers as infinite equivalence classes of pairs of natural numbers. Hell, you can even consider natural numbers as infinite sets. The fact that there is a finite implementation of these concepts makes them finitist.

>> No.15806188

>>15806185
No, finitists don't consider an arbitrary real number to be a legitimate well-defined concept.

>> No.15806196

>>15806188
so they can't make statements about arbitrary real numbers?

>> No.15806202

>>15806186
what is finitist implementation of "all natural numbers"

>> No.15806204

>>15806196
Finitists (including myself) don't know what is meant by a real number. The so-called definitions of Cauchy and Dedekind are not well-founded.

>> No.15806209

>>15806202
All natural numbers are strings of digits 0-9, as I said before.

>> No.15806210

>>15806204
what is the problem with the definitions? and doesn't this exclude a large portion of mathematics from finitists' reach?

>> No.15806217

>>15806209
i was asking about what would be referred to by infinitists as the set of all natural numbers, not what defines a natural number (that it is a string of digits 0-9)

>> No.15806227

>>15806210
The problem is that all known definitions of real numbers crucially rely on the undefined concept of an arbitrary infinite subset of the naturals. The finitist can understand and interpret infinite computable subsets of the naturals as a figure of speech standing for algorithms which determine whether or not a given natural number belongs to that set. They can even make sense of uncomputable but still arithmetic sets, for example the set of all natural numbers which encode an algorithm (given a suitable encoding) that halts, by viewing them as a figure of speech that stands for the property that defines them. However, the finitist doesn't know what is meant by an infinite set that is neither computable nor arithmetical. It's like talking about an undefinable set. Doesn't make much sense.

>> No.15806228 [DELETED] 

>60 posts
>17 IPs
just OP cringe bumping his vanity thread over and over again

>> No.15806239

>>15806217
Finitists don't view the natural numbers as part of a single completed set (completed infinity). However a statement about the set of natural numbers that doesn't involve other arbitrary infinite sets, can be quite easily translated to be understood by finitists to be a statement about the natural numbers themselves.

>> No.15806286

>>15806228
I literally have not replied to this thread since I made it. I haven't even read these comments

>> No.15807123

So many simple questions.

Finitism is best defined as a prefence to axiomatic approach that avoids "infinite" objects carefully.

To a "finitist", it makes more sense that we don't allow such thing as "Axiom of Infinity" than the opposite.

The exact methods we use to avoid infinity can vary. There are many things that can go infinite. Many different techniques to remain finite, not all being equally rigorous.

>> No.15807482

>>15806227
This is not true since real numbers can be dealt with WKL0 or RCA0, which are fragments of second order arithmetics which are **conservative** over I Sigma_1 (a fragment of Peano). A real number is here just a subset of the set of natural numbers HOWEVER whenever you prove something about natural numbers, all talk about real numbers or more can be viewed as a scaffolding you remove.

>> No.15807488

Dumb argument. Anything infinite can be made finite for all practical purposes by adding the caveat "that humans will ever conceive of/have use for." The set of natural numbers is infinite. Don't belive in infinite sets? Fine, take the set of natural numbers that humans will ever use, that's finite and the difference between that and the actual set of natural numbers by definition will never matter to us.

>> No.15807495

>>15807482
>This is not true
What is not true?
>since real numbers can be dealt with WKL0 or RCA0
What does it mean to deal real numbers?

>> No.15808335

>>15806227
>>15806204
>The so-called definitions of Cauchy and Dedekind are not well-founded
>The problem is that all known definitions of real numbers crucially rely on the undefined concept of an arbitrary infinite subset of the naturals
Do you reject function objects too? That's dumb. What you should reject is the notion of Cauchy/Dedekind numbers as having independent existence from the theory they're stated within.

>> No.15808737

>>15803959
>the usual math systems (set theory, type theory, arithmetic) hadn't been found to be inconsistent so far.
Yes they have Russel's Paradox infers self contradiction in the foundation all formal systems, (arithmetic is inconsistent at -0=0 because that would make 0 its own opposite number and both positive and negative while set theory starts at an empty set that can't actually be empty if it contains itself) which was he created type theory, but even then you just kind of avoid answering what type of type is type instead of coming up with a solid logical grounding for its foundational element.

>> No.15810010

>>15807123
How do you integrate without infinity? Limits are infinity.

>> No.15810314

>>15810010
You just deal with sums [math]\sum_{i=1}^n ... [/math] I guess