/sci/ - Science & Math

[Anonymous No.8705874]

What does /sci/ think of intuitionistic logic and mathematical constructivism?

[Anonymous No.8706145]

>>8705874
I think it's a fucking pain in the ass because I'm stuck on the first problem of my metalogic homework. Proving shit within a language is just easy rubiks cube puzzle shit where you shuffle stuff around; anyone who's smart enough to do basic algebra can do that, but proving things about formal languages themselves is just fucking weird because I'm never sure if I'm essentially just begging the question. I don't get why I can just whip up a language to talk about the language I just whipped up, it feels like I'm just kicking the can down the road.

[Anonymous No.8707153]

>>8705874
prtty much god tier.
It's why linguistics is better than math.
Symbolism and semantics

[Anonymous No.8707155]

>>8705874
It's autistic bullshit and this is coming from somebody working with ATPs.

Fuck dependent types, while I'm at it

[Anonymous No.8707181]

>>8705874
What is this?
>P or not p
>Not not p

[Anonymous No.8707202]

from wikipedia:
>In particular, systems of intuitionistic logic do not include the law of the excluded middle and double negation elimination
Anyone could explain what's the reasoning behind that, and what problem does it solve?

[Anonymous No.8707203]

>>8707181
claims that get weaker

Fix a claim p.

- absudity proves anything

in particular
- absudity proves p
- absudity proves not p

- p proves not(not p)
- p proves (p or not p)
classically the last one would be true always, though

-(not p) proves (p or not p) as well
As a special case of
>p proves not(not p)
you have that
-(not p) proves not(not(not p))

...

[Anonymous No.8707206]

>>8707202
I'll repost my answer from a thread a few weeks ago (without re-reading it)

---

>Classical predicate logic maintains the principle of excluded middle (LEM) as axiomatic, so what are the arguments for why mathematics should privilege a different logical basis?

As the other anon points out, it's not a question of disregarding richer and "more careless" axiomatic frameworks, it's a matter of application.
If you reason about a subject that includes the statement
>It's true that today I'll eat at MacDonalds OR it's false that today I'll eat at MacDonalds
i.e. [math]M \lor \neg M[/math] where the semantics (I should maybe say 'subject', as semantics is used more technically too) of [math]M[/math] are "today I'll eat at MacDonalds ".
then adoption LEM is likely what you want to do.
If you reason about a subject that includes the statement
>It's the case that the talking stone is blue OR it's not the case that the talking stone is blue
I'm not sure anymore.

If you drop LEM, then your theory necessarily proves less theorems. What's nice is that you can then also adopt new non-constructive axioms, which if together with LEM would have produces an inconsistency. I.e. there are interesting theories which you can't axiomize in classical logic because of this.
Pic related is a theory of smooth closeness which breaks down by adding the nonconstructive LEM
https://en.wikipedia.org/wiki/Synthetic_differential_geometry

The message here is that by adopting this rule of inference, you actually choose the math you work with: given the axioms which are about the semantical things proper (vector space laws, MacDonalds laws, etc.) you also define that theories by the rules of inference you use. I.e. you narrowed down the range of possible theories by doing actively deciding the rules of logic. That's why it's interesting to see which part of functional analysis, say, does still hold in the weaker world of reasoning.

[Anonymous No.8707212]

Why drop LEM and not some other law in classical logic? Why is LEM termed the nonconstructive one.

An appealing aspect of intuitionistic logic is that is has faithful semantics (in the sense of: let [math]M[/math] mean that „today I'll eat at MacDonals.“) in something real, namely actions.

https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%93Kolmogorov_interpretation

https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence

This logic is precisely the one which you can use to describe a cooking recopy or a programming language:

Read [math]A \land B[/math] (interpretation in logic: „it’s true that A holds and it’s true that B holds“) as
>I have a proof/reason to believe/argument for A and I have a proof/reason to believe/argument B
Read [math]A \lor B[/math] in the same way.
Read [math]A \to B[/math] (in logic: „if A is true, then B is true„) as
>If I have proof/reason to believe/argument for A, then I can conceive a proof/reason to believe/argument
and [math]\neg A[/math] (in logic „A is false“) as
>If I have proof/reason to believe/argument for A, then something’s wrong because that’s a contradiction and doesn’t make sense
The last connective is properly defined as [math]\neg A := A \to \bot[/math]

Now a statement like
[math](A \land B) \to A[/math]
is intutionistically true, because if I have a reason to believe A and one to believe B, then in particular I have a reason to believe A. Computationally, this „proof I just give corresponds to a function [math]f[/math] of type
[math](A \times B) \to A[/math]
i.e.
[math]f : (A \times B) \to A[/math]
namely
[math]f = \langle a, b\rangle \mapsto a[/math]
or written differently,
[math]f = p \mapsto \pi_1(p)[/math],
where [math]\pi_l[/math] is the left projection operation.

[Anonymous No.8707215]

A reason g not to believe A, i.e.
[math]g: \neg A[/math] or [math]g: A\to \bot[/math]
can be read as a function that takes an argument a and A but never terminates. g(a) is looping on your hard drive forever.

The statement [math]A \to \neg ( \neg A )[/math] is also true: Having a reason to believe A means that also having a reason not to believe A would already be a contradiction.
The computational proof [math]h : A \to ( (A \to \bot) \to \bot) [/math] is simple too:
[math]h = a \mapsto ( H \mapsto H(a) )[/math]
Given an argument ‚a‘ and then a looping function [math] H : A\to \bot [/math], plugging in ‚a‘ into H will trigger an unending loop - the type matches.

But [math](A\to \bot) \to \bot \to A[/math] is constructively not true. To logical argument is this: Merely knowing that ‚a reason to believe A is absurd‘ would be absurd - this in itself is not a constructive argument for A.
Maybe the computational semantics is more clear here: Asking for a function of type
[math]( ( A \to \bot ) \to \bot) \to A[/math]
is asking for way to construct a term ‚a‘ using a functional which takes looping functions in [math]A \to \bot[/math] as argument but never terminates. How would a terms ‚a‘ ever come from this?? It doesn’t.

A more complicated but not too hard example, to conclude this, would be
[math] ( \neg A \land \neg B ) \implies \neg ( A \lor B ) [/math]
>If ‚A is false‘ as well as ‚B is false‘, then neither is 'A or B'.
or
[math] ( ( A \to \bot) \times ( B \to \bot ) ) \to (A+B) \to \bot [/math]
where + is the direct sum.
If next to the projection operators you introduce the programming concept of if-clauses now (as you have them in C++ or Phython), you’ll be able to proof this claim.

Indeed, provability and programability coincide now, that’s the pretty thing.

[Anonymous No.8707219]

>>7708352
If by "analysist" you mean a guy who's studying classical analysis, then the question has probably no answer.
Dropping non-constructive axioms of your theories becomes relevant, for example, whenever you got to implement stuff. As you can't even list the element of [math]\mathbb R[/math], theorems in classical analysis will be vacuous for such realization. The good news is that people have spun the spiderwebs of theories like analysis in a constructive fashion long ago, see for example all the constrictive theorems that aggregate around the unprovable intermediate value theorem

https://en.wikipedia.org/wiki/Constructive_analysis#Examples

Syntetic analysis as in the pic from the book by Kock is relevant because the requirements for the theory are such that certain topoi give you internal analysis as a gift. That is you consider some topos, check if it has this and that property and then it might be implied that that topos really is about calculus/contains a theory of calculus and you can import all the theorems you already know - I mean that's the nice feat of category theory in general.

The category of sets [math]A, B, C,...[/math] (=objects) and functions [math]f, g ,h,...[/math] (=arrows) is a topos and thus has cartesian product [math]A\times B[/math] (=the categorical product) and function spaces [math]B^A[/math] (=internal, setty realizations of the arrow class from [math]A[/math] to [math]B[/math], which may be written [math]A \to B[/math])
A theorem of sets is that the function space
[math] (A\times B) \to C [/math]
is isomorphic to
[math] (B\times A) \to C [/math]
as well as
[math] A \to C^B [/math]
and
[math] B \to C^A [/math]
E.g. for A=B=C the reals the first space contains
[math] \langle a,b \rangle \mapsto \sin(a)+3b [/math]
which you can systematically map to the function
[math] \langle b,a \rangle \mapsto \sin(a)+3b [/math]

[Anonymous No.8707222]

in the second space, or the function
[math] a \mapsto (b \mapsto \sin(a)+3b) [/math]
or
[math] b \mapsto (a \mapsto \sin(a)+3b) [/math]

The axioms of a topos have more than the sets as model, for example it provides an (intuitionistic logic), where the iso above means
„A and B being true implies C“
is equivalent to
„A being true implies B being true implies C“

Or you can take the classical identifications of the set theoretic operations as numerical operations. Forgetting what your finite sets are about, the above relation is the basic identity of numbers
[math] c^{a·b} = {c^a}^b [/math]
In the other direction, the relation
[math] c^{a+b} = c^a·c^b [/math]
provable in a topic, at the same time tells you for the categories of sets (where + is the disjoint/tagged union) that the function space
[math] (A+B) \to C [/math]
is iso (i.e. in bijection to) to
[math] (A\to C) \times (B\to C) [/math]
In logic,
„one of A or B being true already implies C“
is equivalent to
„A implies C and also B implies C“

In the other direction, a derivation rule like modus p.
„From A and A implies B follows B“
being true guarantees you that the function space
[math](A\times B^A)\to B[/math]
isn’t empty
Indeed, the evaluation function
[math] eval (a,f) := f(a) [/math]
works no matter which sets A and B are.

What I want to say is this: Formulating analysis synthetically in a basic object like a topos (as opposed to something hard to construct like R), makes theorems of analysis more than theorems of just analysis. And secondly, if you know that analysis works if a topos has this and that axioms, then you can further build your theory (like quantum field theory, kek) in such a setting without restricting you to muh reals and muh epsilons. Although the reals are nice of course.

---

There was more but I'm not sure if this actually answers your question

[Anonymous No.8707235]

>>8707222
Well one more thing, a remark about the double-negation translation:

When it comes to classically interpreted propositions, classical propositional logic and intuitionistic propositional logic have the same proof strength (although proving theorems in classical logic might be more straight forward). This is because if the former proves P, then the latter always proves classically equivalent statements such as ¬¬P (and the converse of this is trivial). So to prove any (classically provable) theorem P, you can start out and stick to the intuitionistic framework the whole time, up until the end where, having proven ¬¬P intuitionistically, you apply an non-constructive (purely classical) translation such as ¬¬P→P.

pic related, a constructive proof of a theorem that is the law of excluded (LEM) in classical logic.

This can be extended to a theory with existential quantifier. It can also be extended to the universal quantifier, except the translaion is more intricate.

[Anonymous No.8707240]

>>8707215
>Indeed, provability and programability coincide now, that’s the pretty thing.
Thanks anon, some of that was a bit over my head but I appreciate this last statement.

[Anonymous No.8707257]

>>8707240
This aspect is buried in the second part, where I link to the Curry-Howard correspondence

https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence

The pic in the last post should give a good example of this:
On the one hand, we have the logical statement
>forall A. forall B. ((A→B)∧((A→B)→B))→B
saying
>for all proposition A and B, we have that
>if (A implies B) holds and if ((A implies B) implies B) holds, then B holds
on the other hand, we have, for generic type A and B, the type
((A→B)×((A→B)→B))→B
and a function F which has that type is
F((f, G)) := G(f)
(you can do pattern matching in your head to see that, in the argument pair (f,G), the entry f a function of type A→B and G is a functional of type (A→B)→B, so that G(f) is indeed a term of type B)

The correspondence says that exactly the logical statements in constructive/intuistionistic logic are the ones which can be proven by finding a function for a type.
This is in turn the same as saying "A or (not A)" is that crucial statement which doesn't have a reading in terms of functions.

[Anonymous No.8707341]

>>8707155
Martin-Löf is love, ML is life.

[Anonymous No.8707366]

supreme autism

[Anonymous No.8707373]