/sci/ - Science & Math » Thread #14048991

12KiB, 519x86, rigorousbtw.png

View Same Google iqdb SauceNAO

Calling all set theorists: what even is a set?

Anonymous Sun 02 Jan 22:50:48 2022 No.14048991 View Reply Original Report

Quoted By: >>14049012 >>14049038 >>14049084 >>14049702 >>14051676 >>14051869 >>14052746

Anonymous

Anonymous Sun 02 Jan 2022 22:56:45 No.14049012 Report

Quoted By: >>14049018

>>14048991
This is a philosophical question, math can't give a good answer

Anonymous

Anonymous Sun 02 Jan 2022 22:59:24 No.14049018 Report

Quoted By: >>14049033

>>14049012
cop out answer

Anonymous

Anonymous Sun 02 Jan 2022 23:02:15 No.14049032 Report

Quoted By: >>14049045 >>14049191 >>14051706

I had a revelation yesterday. I don't know what it's worth though.

Lambda calculus encode integers via Church numerals

A Turing Machine encode integers as symbols of the alphabet (I think)

In set theory, there is this weird encoding, I don't know what it's called or what it is exactly. But it also has an encoding for integers. I've seen it in the video of a course. I can find it if need to.

And I guess that from integers, we can build on top a big chunk of mathematics.
I think it's interesting because it shows a similarity between models of computation and one of the axiomatic system that serves as foundation to mathematics.

I will be thinking on what that means for some time. Until maybe I have another revelation or find the right piece of information.

Anonymous

Anonymous Sun 02 Jan 2022 23:02:27 No.14049033 Report

Quoted By:

>>14049018
explain how this isnt a philosophical question

Anonymous

Anonymous Sun 02 Jan 2022 23:03:36 No.14049038 Report

Quoted By:

>>14048991
useful notation

Anonymous

Anonymous Sun 02 Jan 2022 23:05:05 No.14049045 Report

Quoted By: >>14049066

>>14049032
>it shows a similarity between models of computation and one of the axiomatic system that serves as foundation to mathematics.
yes it called a formal system

Anonymous

Anonymous Sun 02 Jan 2022 23:11:51 No.14049066 Report

Quoted By: >>14049079

>>14049045
All 3 are formal systems. Alright.
You mean that Lambda Calculus and the Turing machine can serve as a foundation of mathematics in the place of set theory?

Anonymous

Anonymous Sun 02 Jan 2022 23:16:32 No.14049079 Report

Quoted By:

>>14049066
yes, but like you said only systems that encode our intuition of the basic integers are really useful.

Anonymous

Anonymous Sun 02 Jan 2022 23:18:29 No.14049084 Report

Quoted By:

>>14048991
a unit of something

Anonymous

Anonymous Sun 02 Jan 2022 23:24:59 No.14049104 Report

Quoted By: >>14049175 >>14051706 >>14052746

I mean, when I remembered that integers had an encoding in set theory, I was like: Wow. We absolutely don't care what a set is. What counts is that we can encode integers in it, and its operations on it. What counts is that we have a system in which we can encode mathematical objects with the algebraic properties that we want. And it is as uglier that LC and TM, but it works.
So set theory (+ logic?) is doing the same thing that models of computations. What?

I heard that first order logic is Turing complete.

So in maths you define things, apply some inference rules/axioms, and demonstrate some proposition or theorem. And you're doing something similar in lambda calculus. You define/encode numbers, plus operations. And then you can combine this operations and compute stuff.

So proofs are the same as evaluation of programs.
Am I right? Is this really the Curry-Howard correspondence right here ?

Anonymous

Anonymous Sun 02 Jan 2022 23:48:18 No.14049175 Report

Quoted By: >>14049203

>>14049104
>So set theory (+ logic?) is doing the same thing that models of computations. What?
yes, for any provable theorem in set theory, and consequently all mathematics, there exists a computer program that generates that theorem.

Am I right? Is this really the Curry-Howard correspondence right here ?
yes

Anonymous

Anonymous Sun 02 Jan 2022 23:54:53 No.14049191 Report

Quoted By:

>>14049032
>In set theory, there is this weird encoding
von Neumann ordinals:
$0:=\{\},$ $1:=\{\{\}\},$ $2:=\{\{\},\{\{\}\}\},$ $3:=\{\{\},\{\{\}\},\{\{\},\{\{\}\}\}\},$
etc.
Then the successor function is defined as $S(n)=n\cup \{n\}$

Anonymous

Anonymous Sun 02 Jan 2022 23:57:59 No.14049203 Report

Quoted By: >>14052746

>>14049175
Awesome.
Is the inverse true ?
For every computer program there is a corresponding proof ?

Anonymous

Anonymous Mon 03 Jan 2022 00:14:19 No.14049255 Report

Quoted By:

If this is true, given that automated proof generation is basically searching a infinite combinatorial space, this means that the halting problem can be expressed as the different outcomes of the search process.

Anonymous

Anonymous Mon 03 Jan 2022 00:19:29 No.14049267 Report

Quoted By:

Decidability, completeness, incompleteness are also near. Maybe even P vs NP, and the time VS space tradeoff

Anonymous

Anonymous Mon 03 Jan 2022 00:47:17 No.14049368 Report

Quoted By:

The infinite combinatorial space is an infinite graph. A node is a proposition (or a finite set of proposition). An edge is the application of one or more inference rules/axiom to transform the proposition into another. Proving a proposition means finding a path.

And if the process of finding a path is the same as evaluating a program/compute something, this means that the more steps you have to make to arrive at the proposition/result of computation, the more time you take. So different paths that goes more or less directly to the end destination, means different times of execution of the same algorithm. The time of an algorithm is the path on that graph.
So space as in time vs space, eg memory, would be the content of a node. Which represents a proposition, which is just an expression (first order logic). Which can be viewed as an AST.
When we hop from node to node, the proposition change. The expression get bigger and smaller, hence take more or less memory. The biggest proposition along the path is how much the algorithm takes in memory.
If we see the infinite graph (space) as an (x,y) plane, and the size of an the proposition of each node as a z point, we get some sort of landscape for the given algorithm.
The time vs space tradeoff probably means that, if we take the shortest path to the result of the computation, there should be a "mountain". (If time shrinks, space/memory should grow) and taking the contour of the "mountain" assure to always stays at a low altitude, but require taking a longer path. (So space/memory shrinks, time grows)

I am on fire.

Anonymous

Anonymous Mon 03 Jan 2022 00:54:28 No.14049390 Report

Quoted By:

I need to make a data science project to verify my hypothesis by visualization.
I guess what is needed is a way to transform an imperative / functional program into prolog maybe

Anonymous

Anonymous Mon 03 Jan 2022 02:21:09 No.14049702 Report

Quoted By:

>>14048991
t.setlet

Anonymous

Anonymous Mon 03 Jan 2022 07:36:43 No.14050715 Report

Quoted By: >>14051692

The answer is yes. I can't believe this is so hard for people to understand. If you can for any reason think to yourself "is this a set?" YES! Fuck, it's not hard.

Anonymous

Anonymous Mon 03 Jan 2022 14:42:01 No.14051676 Report

Quoted By:

>>14048991
An element with a defined relationship/limitations.
An element is any form of distinction or limitation in a medium.
A medium is an element.

Anonymous

Anonymous Mon 03 Jan 2022 14:49:21 No.14051692 Report

Quoted By:

>>14050715
is the set of all sets that do not contain itself a set?
russell says no

Anonymous

Anonymous Mon 03 Jan 2022 14:55:07 No.14051706 Report

Quoted By: >>14051876

>>14049032
>>14049104

yes, lambda calc/turing machines can serve as the basis of a mathematical system. It's in the name *calculus*. At its core these calculi just perform logical operations, and we can encode proofs in them thus constructing mathematics as we know it (we can also do this with integers, see [1]).
In fact, lambda calculus was first developed as a way to formally ground mathematics, but was later shown to be inconsistent by Kleene.

[1] https://en.wikipedia.org/wiki/G%C3%B6del_numbering

Anonymous

Anonymous Mon 03 Jan 2022 15:50:24 No.14051869 Report

Quoted By: >>14052746

>>14048991
a set is a collection of sets

Anonymous

Anonymous Mon 03 Jan 2022 15:52:41 No.14051876 Report

Quoted By:

>>14051706
>lambda calc/turing machines can serve as the basis of a mathematical system
Lambda calculus can't serve as a basis for mathematics because it's inconsistent. The thing that makes it inconsistent is the same thing that makes it Turing-complete. Turing machines can't serve as the basis of mathematical systems, either.

Anonymous

Anonymous Mon 03 Jan 2022 20:20:10 No.14052746 Report

Quoted By:

>>14048991
A class is a collection: an entity for which, for any given thing, it is well-determined whether that thing is an element of it.
A set is a class that is an element of some class.
>>14049104
The CH correspondence is essentially:
theorems ~ types
proofs ~ programs
So a program encodes a proof of its type.
For example:
If x corresponds to a proof of A and y corresponds to a proof of B, then the ordered pair <x, y> corresponds to a proof of A & B.
>>14049203
The computer program encodes the proof.
>>14051869
The collection of all ordinals is a collection of sets but not a set, by the Burali-Forti paradox.

Capcode	All Only User Posts Only Moderator Posts Only Admin Posts Only Developer Posts
Show Posts	All Only With Images Only Without Images
Deleted Posts	All Only Deleted Posts Only Non-Deleted Posts
Ghost Posts	All Only Ghost Posts Only Non-Ghost Posts
Post Type	All Only Sticky Threads Only Opening Posts Only Reply Posts
Results	All Grouped By Threads
Order	Latest Posts First Oldest Posts First

Your latest searches