Last active
November 14, 2017 06:30
-
-
Save ericTsiliacos/ef6562a46f30c7bfa6dadd5c5f5d580a to your computer and use it in GitHub Desktop.
Understanding
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- "I agree with you that it is important once and | |
-- for all to examine all of our assumptions in order | |
-- to establish something solid." - Letter to Foucher by Leibniz | |
-- Break down propositions into defintions (recusively) until one arrives at identities who are called such | |
-- because their defintions are necessary truths (or non-contradiction). | |
-- Question(s): Are the natures or essences of things necessary truths? Is it provable? | |
-- Using the "for all" qualifity, one can arrive at the essence of a thing? | |
-- But there lies a contradictions: How would one to include an object into | |
-- the set of elements one is trying to describe without having already | |
-- known it belonged in the set? From whence does this ability come from? | |
-- Are we merely abstracting out the differences between objects? | |
-- For depending on which two object one compares, or the ordering one chooses | |
-- one might arrive at a different abstraction. | |
-- It could be thought of as the uses of objects that bring them together | |
-- and for a particular purpose that then an abstraction is discovered. | |
-- In nature, does one observe many objects of various kinds, | |
-- as Scipture points to the nature or form of created things - | |
-- "according to its [or their] kind". | |
-- "There are two things that should be distinguished in every argument, namely, form and subject matter." | |
-- - Samples of the Numerical Characterisic | |
-- http://yogsototh.github.io/Category-Theory-Presentation/#slide-46 | |
-- https://people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf | |
-- Sum types (or): Closed universe | |
-- Product types (and) | |
-- Exponential types (functions) | |
-- Recursive types (recusive functions) | |
-- Necessary truths and contingent truths | |
-- Types are structural | |
id :: x -> x | |
id x = x |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment