Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
intuitionistic_propositional_logic [2016/04/13 11:20] nikolaj |
intuitionistic_propositional_logic [2017/01/07 01:12] 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. | ||
| Line 307: | Line 307: | ||
| In fact, take any $A,B$ and observe that | In fact, take any $A,B$ and observe that | ||
| - | $(A\to B)\land((A\to B)\to B)\to B$ | + | $((A\to B)\land((A\to B)\to B))\to B$ |
| "If it's the case that '$A$ implies $B$' and also that '$A$ implies $B$' implies $B$, then $B$ is the case." | "If it's the case that '$A$ implies $B$' and also that '$A$ implies $B$' implies $B$, then $B$ is the case." | ||
