Differences

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

Link to this comparison view

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 Mwhere the semantics (I should maybe say '​subject',​ as semantics is used more technically too) of $Mare "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 $Mmean 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 Bin 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 ​$fof 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_lis 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 Aor $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 Ais 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 \botas 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 $Ato $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. 
  
Link to graph
Log In
Improvements of the human condition