# Differences

This shows you the differences between two versions of the page.

Both sides previous revision Previous revision | |||

intuitionistic_propositional_logic [2016/08/28 01:17] nikolaj |
intuitionistic_propositional_logic [2017/01/07 01:12] (current) nikolaj |
||
---|---|---|---|

Line 161: | Line 161: | ||

If you reason about a subject that includes the statement | 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 | >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 ". | + | i.e. $M \lor \neg M$ where the semantics (I should maybe say 'subject', as semantics is used more technically too) of $M$ are "today I'll eat at MacDonalds ". |

then adoption LEM is likely what you want to do. | then adoption LEM is likely what you want to do. | ||

If you reason about a subject that includes the statement | If you reason about a subject that includes the statement | ||

Line 177: | Line 177: | ||

- | 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. | + | An appealing aspect of intuitionistic logic is that is has faithful semantics (in the sense of: let $M$ 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/Brouwer%E2%80%93Heyting%E2%80%93Kolmogorov_interpretation | ||

Line 185: | Line 185: | ||

This logic is precisely the one which you can use to describe a cooking recopy or a programming language: | 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 | + | Read $A \land B$ (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 | >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 $A \lor B$ in the same way. |

- | Read [math]A \to B[/math] (in logic: „if A is true, then B is true„) as | + | Read $A \to B$ (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 | >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 | + | and $\neg A$ (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 | >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] | + | The last connective is properly defined as $\neg A := A \to \bot$ |

Now a statement like | Now a statement like | ||

- | [math](A \land B) \to A[/math] | + | $(A \land B) \to A$ |

- | 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 | + | 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 $f$ of type |

- | [math](A \times B) \to A[/math] | + | $(A \times B) \to A$ |

i.e. | i.e. | ||

- | [math]f : (A \times B) \to A[/math] | + | $f : (A \times B) \to A$ |

namely | namely | ||

- | [math]f = \langle a, b\rangle \mapsto a[/math] | + | $f = \langle a, b\rangle \mapsto a$ |

or written differently, | or written differently, | ||

- | [math]f = p \mapsto \pi_1(p)[/math], | + | $f = p \mapsto \pi_1(p)$, |

- | where [math]\pi_l[/math] is the left projection operation. | + | where $\pi_l$ is the left projection operation. |

A reason g not to believe A, i.e. | A reason g not to believe A, i.e. | ||

- | [math]g: \neg A[/math] or [math]g: A\to \bot[/math] | + | $g: \neg A$ or $g: A\to \bot$ |

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. | 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 statement $A \to \neg ( \neg A )$ 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: | + | The computational proof $h : A \to ( (A \to \bot) \to \bot) $ is simple too: |

- | [math]h = a \mapsto ( H \mapsto H(a) )[/math] | + | $h = a \mapsto ( H \mapsto H(a) )$ |

- | 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. | + | Given an argument ‚a‘ and then a looping function $ H : A\to \bot $, 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. | + | But $(A\to \bot) \to \bot \to A$ 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 | Maybe the computational semantics is more clear here: Asking for a function of type | ||

- | [math]( ( A \to \bot ) \to \bot) \to A[/math] | + | $( ( A \to \bot ) \to \bot) \to A$ |

- | 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. | + | is asking for way to construct a term ‚a‘ using a functional which takes looping functions in $A \to \bot$ 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 | 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] | + | $ ( \neg A \land \neg B ) \implies \neg ( A \lor B ) $ |

>If ‚A is false‘ as well as ‚B is false‘, then neither is 'A or B'. | >If ‚A is false‘ as well as ‚B is false‘, then neither is 'A or B'. | ||

or | or | ||

- | [math] ( ( A \to \bot) \times ( B \to \bot ) ) \to (A+B) \to \bot [/math] | + | $ ( ( A \to \bot) \times ( B \to \bot ) ) \to (A+B) \to \bot $ |

where + is the direct sum. | 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. | 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. | ||

Line 232: | Line 232: | ||

>>7708352 | >>7708352 | ||

If by "analysist" you mean a guy who's studying classical analysis, then the question has probably no answer. | 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 | + | 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 $\mathbb R$, 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 | https://en.wikipedia.org/wiki/Constructive_analysis#Examples | ||

Line 238: | Line 238: | ||

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. | 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]) | + | The category of sets $A, B, C,...$ (=objects) and functions $f, g ,h,...$ (=arrows) is a topos and thus has cartesian product $A\times B$ (=the categorical product) and function spaces $B^A$ (=internal, setty realizations of the arrow class from $A$ to $B$, which may be written $A \to B$) |

A theorem of sets is that the function space | A theorem of sets is that the function space | ||

- | [math] (A\times B) \to C [/math] | + | $ (A\times B) \to C $ |

is isomorphic to | is isomorphic to | ||

- | [math] (B\times A) \to C [/math] | + | $ (B\times A) \to C $ |

as well as | as well as | ||

- | [math] A \to C^B [/math] | + | $ A \to C^B $ |

and | and | ||

- | [math] B \to C^A [/math] | + | $ B \to C^A $ |

E.g. for A=B=C the reals the first space contains | E.g. for A=B=C the reals the first space contains | ||

- | [math] \langle a,b \rangle \mapsto \sin(a)+3b [/math] | + | $ \langle a,b \rangle \mapsto \sin(a)+3b $ |

which you can systematically map to the function | which you can systematically map to the function | ||

- | [math] \langle b,a \rangle \mapsto \sin(a)+3b [/math] | + | $ \langle b,a \rangle \mapsto \sin(a)+3b $ |

in the second space, or the function | in the second space, or the function | ||

- | [math] a \mapsto (b \mapsto \sin(a)+3b) [/math] | + | $ a \mapsto (b \mapsto \sin(a)+3b) $ |

or | or | ||

- | [math] b \mapsto (a \mapsto \sin(a)+3b) [/math] | + | $ b \mapsto (a \mapsto \sin(a)+3b) $ |

The axioms of a topos have more than the sets as model, for example it provides an (intuitionistic logic), where the iso above means | The axioms of a topos have more than the sets as model, for example it provides an (intuitionistic logic), where the iso above means | ||

Line 262: | Line 262: | ||

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 | 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] | + | $ c^{a·b} = {c^a}^b $ |

In the other direction, the relation | In the other direction, the relation | ||

- | [math] c^{a+b} = c^a·c^b [/math] | + | $ c^{a+b} = c^a·c^b $ |

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 | 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] | + | $ (A+B) \to C $ |

is iso (i.e. in bijection to) to | is iso (i.e. in bijection to) to | ||

- | [math] (A\to C) \times (B\to C) [/math] | + | $ (A\to C) \times (B\to C) $ |

In logic, | In logic, | ||

„one of A or B being true already implies C“ | „one of A or B being true already implies C“ | ||

Line 277: | Line 277: | ||

„From A and A implies B follows B“ | „From A and A implies B follows B“ | ||

being true guarantees you that the function space | being true guarantees you that the function space | ||

- | [math](A\times B^A)\to B[/math] | + | $(A\times B^A)\to B$ |

isn’t empty | isn’t empty | ||

Indeed, the evaluation function | Indeed, the evaluation function | ||

- | [math] eval (a,f) := f(a) [/math] | + | $ eval (a,f) := f(a) $ |

works no matter which sets A and B are. | works no matter which sets A and B are. | ||