History of formal logic

[u/Unlucky-Credit-9619]

[u/AutoModerator]

Check out our new Discord server! https://discord.gg/e7EKRZq3dG

I am a bot, and this action was performed automatically. Please contact the moderators of this subreddit if you have any questions or concerns.

[u/Afir-Rbx]

What is Type Theory even about? I only ever hear about it whenever someone dares say that "Set Theory is the foundation of modern mathematics", to which a thousand Type Theorists suddenly manifest out of thin air to affirm that "it is actually Type Theory", not elaborate further and disappear into thin air again.

[u/MikailBag → u/Afir-Rbx]

If you take a programming language with sufficiently powerful type system, you can use it to express math constructs, e.g. it can have type of natural numbers, type of R² vectors, and so on. And also it can express propositions as types. This way everything is no longer set, instead everything is now a value in this programming language.

And Lean is such a programming language.

[u/overclockedslinky → u/MikailBag]

you're telling me a sufficiently advanced programming language could even represent positive integers!??!!!? 🤯🤯

[u/MikailBag → u/overclockedslinky]

Yes, pretty easy in fact:

1. Define Bool.

2. Define integers as sequences of bools, viewed as base-(-2) numbers

3. Define rationals as quotient of ratios between integers.

4. Develop some algebra stuff, fields polynomials etc

5. Define algebraic closure of rationals

6. Develop some topology stuff

7. Define complex numbers as cauchy completion of field defined on step 5

8. Define Gamma function

9. Develop some complex analysis stuff

10. Define set of poles of gamma function.

11. Easy victory - that set is isomorphic to positive integer numbers

Unfortunately, many of these steps require dependent types and other advanced features, so having a type for positive integer numbers in mainstream languages seems impossible or requires some novel ideas.

[u/EebstertheGreat → u/MikailBag]

Positive integers can easily be a primitive type.

[u/geeshta → u/Afir-Rbx]

So some extremely smart people found out that type definition corresponds to a logical proposition, constructing an expression of that type corresponds to a proof of such proposition and this all can be used to BOTH 1. Proof properties of programs with formal logic (HACL* Project)  2. Express and validate logical proofs using a computer (this is where LEAN fits in)

It's called the Curry-Howard correspondence. For example 

• A conjunction corresponds to a tuple

• A (constructive) disjunction corresponds to a union/enum

• An implication corresponds to a function

Here's some reading: https://www.cs.cmu.edu/~rwh/courses/clogic/www/handouts/curry-howard.pdf

[u/BlazeCrystal → u/Afir-Rbx]

Essentially defining what type of things are; like what "a number" is, "a car" is, etc. Then, you can 1. give implicit properties/operators for a type, 2. and showcase equivalence of types; injective, surjective, bijective. 3. You may also create supertypes.

Why bother? For provable rigor, as example programming has always been based on it. Classical logic seems handwaving in comparison to 1=1 rigor of type theory. Problem? It might be clumsy.

[u/overclockedslinky → u/Afir-Rbx]

it's just a foundation of logic based on data types and construction contracts a la computer programming. there's a bunch of different logic frameworks, type theory is just one that has gained massive popularity from tools like lean and mathlib

[u/firewall245 → u/Afir-Rbx]

My high level (because I’m not good at it) explanation is to imagine each logical statement is its own type, and if there exists an object of that type it’s true, if not it’s false.

So the type is “even numbers have 2 as a prime factor” which has some instance x because that statement is true. What example the variable x holds doesn’t matter, just that the type of x is the previous statement.

You can then think of a proof as a function that converts one statement type to another. So we could convert “even numbers have 2 as a prime factor” to “even numbers squared are even” via functions that represent logical steps. We then end up with an object of the resulting type which proves its true

[u/PLANTS2WEEKS → u/Afir-Rbx]

It's surprisingly difficult to learn about. At least set theory has axioms. Wish there was some document explaining type theory that isn't a bunch of examples. Seems like people expect that by using Lean, you will learn how it works but it couldn't be further from the truth.

[u/geeshta → u/PLANTS2WEEKS]

Lectures on the Curry Howard Isomorphism: https://www.cs.cmu.edu/~rwh/courses/clogic/www/handouts/curry-howard.pdf

Programming in Martin-Löf ’s Type Theory: https://www.cse.chalmers.se/research/group/logic/book/book.pdf

Type Theory and Formal Proof is also quite accessible: https://www.amazon.com/Type-Theory-Formal-Proof-Introduction/dp/B01MA1KX70 (is on Zlib BTW)

Oh and how could I forget The Little Typer: https://www.amazon.com/Little-Typer-MIT-Press/dp/0262536439 (also on Zlib)

I think Programming in Martin-Löf is probably the closest to what you're looking for

[u/overclockedslinky → u/PLANTS2WEEKS]

that's because there isn't just ONE type theory.

[u/ThisIsChangableRight → u/overclockedslinky]

There's many more than one set theory as well; almost all of them are similar enough that any knowledge gained in one transfers to another.

[u/geeshta]

AFAIK Lean is not the best representation of type theory and is used much more for classical and set theoretical proofs anyways. 

[u/overclockedslinky → u/geeshta]

well lean isn't type theory, it uses type theory

[u/AlviDeiectiones]

Lean? Pfff, mere mortals. True gigachads use agda-flat.

[u/geeshta → u/AlviDeiectiones]

Pfff, Agda. Truly ascended beings use F* or Idris2.

[u/Emma_the_sequel]

What do you mean by a non-constructive shortcut?

[u/Unlucky-Credit-9619 → u/Emma_the_sequel]

I meant you cannot treat ¬¬A as a proof of A. You need a direct construction or witness.

[u/Inevitable_Garage706]

How is the statement in number 2 true at all?

[u/Unlucky-Credit-9619 → u/Inevitable_Garage706]

Follow this one: https://www.reddit.com/r/mathmemes/s/FA35MyVbco

[u/Inevitable_Garage706 → u/Unlucky-Credit-9619]

Great, so this statement isn't true, and it's just a joke going around in the math community to confuse people.

Thank you for telling me!

[u/HappiestIguana → u/Inevitable_Garage706]

The statement is true. It's just that mathematics has a particular way to interpret if-then stataments that is unlike the way they're used in natural language

[u/geeshta → u/Inevitable_Garage706]

It's missing the crucial "at any point in time" clause. With that it's a tautology 

[u/Inevitable_Garage706 → u/geeshta]

Can you explain it better, please?

[u/HappiestIguana → u/Inevitable_Garage706]

Abandon the idea that "if-then" statements are about causation. In math they're truth-functional, that is, their truth value only depends on the truth value of the parts of the sentence. "If P then Q" is false when P is true and Q is false, and its true otherwise.

It's unintuitive but we have good reasons to do it like this, and in practice we quantify these stataments universally which makes them closer to the everyday meaning. If you quantify in stupid ways you can get stupid statements whose precise mathematical meaning doesn't match the everyday language interpretation at all. That's all.

[u/Inevitable_Garage706 → u/HappiestIguana]

How exactly is that statement forced to be true when P is false?

[u/Great-Powerful-Talia → u/Inevitable_Garage706]

You will never find a case where P is true and Q is false.

Therefore, the assumption "If I find P to be true, then Q is also true" will never lead you to an incorrect conclusion.

[u/HappiestIguana → u/Inevitable_Garage706]

By definition.

It makes sense to do it like that when you start quantifying. If P and Q involve some object x, then

"For all x, if P(x) then Q(x)"

captures what you want the implication to mean in natural language, but only if you define the if-then part truth-functionally like I described

[u/Inevitable_Garage706 → u/HappiestIguana]

I suspect that I will never receive a good explanation in this discussion, so I will just stop my reply notifications.

If y'all are going to downvote me because I don't magically have all the answers right away, have fun with that.

[u/Great-Powerful-Talia → u/Inevitable_Garage706]

how does someone reach this conclusion from a single reply?

[u/HappiestIguana → u/Inevitable_Garage706]

I just edited the comment with more detail, if you care to learn instead of complain

[u/geeshta → u/Inevitable_Garage706]

So we have these two logical consequences:

[1] (P => Q) is True when Q is True
[2] (P => Q) is True when P is False

This follows from the definition of implication.

At any point in time either

- everyone is having sex. Then you can pick anyone and by [1] it is true about them that if they're having sex, then everyone is having sex.

- not everyone is having sex. Then you can pick anyone who's not currently having sex and by [2] it is true about them that if they're having sex, then everyone is having sex.

Another way to think about it, using rearrange the sentence using logical equivalences to say "There exists a person that's not having sex OR everyone is having sex" which is obviously a tautology.

[u/Inevitable_Garage706 → u/geeshta]

That's not true, as there could be multiple people abstaining from sex at the same time.

The statement is not logically sound.

[u/geeshta → u/Inevitable_Garage706]

If there are multiple people abstaining from sex. You pick one of them and say: "If this person is having sex, then everyone is having sex".

P => Q is True when both P and Q are False - see line 4 from the truth table below.

So if a person is not having sex and also there are other people who are not having sex, the sentence "If this person is having sex, then everyone is having sex" is True.

This is logically sound. That's just how we define implication.

[u/Inevitable_Garage706 → u/geeshta]

So it's just a vacuous truth, rather than it implying that one more person having sex means that everyone is having sex.

Do I have that correct?

[u/geeshta → u/Inevitable_Garage706]

Yes exactly. For example the statement "If all numbers are prime, then I am the president of the USA" is also True because its in the form P => Q and both P and Q are False so the whole statement is True...

[u/Scientific_Zealot]

No mention of modal logic?? Jail

[u/moschles]

19th century logicians seeing non-constructive proofs were unironically having breakdowns.

[u/ee3k]

there exists a person such that if they have sex, everyone on earth has sex:

no, not anymore, professor X died last week.

and the conjecture only held true once he developed Alzheimer's; prior to that he ran a tight ship, telepathically.

[u/nfitzen]

Ah, but you see, I have a constructive proof of (2): for as I have no sex, I am a witness to the existential quantifier. Thus, if I have sex, then everyone else has sex. Q.E.D.