After an informal history lesson of Set Theory, Category Theory, and Type Theory, we have chosen Type Theory as our foundation moving forward! (Well, actually I chose it, but I'm the professor so you'll have to put up with it).
We saw that Type Theory makes its arguments through a Constructive perspective, whereby we need to find an instance of something happening to understand and define a greater type that objects inform.
Below, we will now get practice with the formal notation used to denote this relationship (And the greater philosophical argument that it represents).
We saw in class that the formal notation for an instance proving the existence of a Type was the following:
In the sub-problems below, give your answers in the exact same format.
Give 5 unique real-world examples of an instance proving the existence of a type
Give 5 unique real-world instances that all prove the existence of the SAME type
Give 5 unique real-world types whose existence is proven by the SAME instance
In class we saw that Type information could be used to intuit the kind of instance we would need to search for to show some greater proposition as valid. Using this type information to guide our search, we could then declare a specific value to make the proposition true. We called this forming a Constructive Proof.
In this problem I would like you to evaluate an expression and give its type. If there is no such instance that can be constructed (You get an absurdity), then briefly explain why no instance within the Type required can make the statement valid.
Use the following information below to answer the sub-problems:
Example 1: Evaluate
Answer:
Example 2: Evaluate
Answer:
Evaluate:
Evaluate:
Evaluate:
Evaluate:
Evaluate:
Evaluate:
Evaluate:
Within the Boolean type, there are special properties that let us simplify larger compound expressions. The questions in this section will be highlighting the interplay between Boolean Algebra on one hand and the Venn Diagram visual system on the other. We know they both have the same ability to display, and prove, properties within the Booleans. Let's investigate some that we did not see in class below!
One of the properties we investigated was the First Complement Law. We showed what it looked like in a table format and a series of venn diagrams. In this problem you must do the same as we did in class, justify the law using a table and venn diagrams, except this time for the Second Complement Law shown below:
Justify the Second Complement Law with a Table
Justify the Second Complement Law with a Venn Diagram
One of the properties we investigated was the First Absorption Law. We showed what it looked like in a table format and a series of venn diagrams. In this problem you must do the same as we did in class, justify the law using a table and venn diagrams, except this time for the Second Absorption Law shown below:
Justify the Second Absorption Law with a Table
Justify the Second Absorption Law with a series of Venn Diagrams
One of the properties we didn't see were the Annihilator Laws for Conjunction and Disjunction. In this problem you must do the same as we did in class, justify the laws with tables and venn diagrams, and also give a small explanation as to why these laws hold:
Justify the Annihilator Laws with Tables
Justify the Annihilator Laws with a series of Venn Diagrams
In class we discovered the properties of operators by performing a deep dive into Addition with the help of 2 visual systems and an algebraic one. These systems were the dots with groups, number line, and typical algebra.
However, the investigation we performed need not only have been done on Addition! You could do it for any operator to discover the properties that they have! We will do the same here, but this time for Multiplication and Subtraction!
Here you will only need to use typical algebra and the number line, we can leave the dots with groups system for another time!
The Associative Property is obtained by an operator between instances when the evaluation order amongst 3 or more of the instances, chained by that operator, does not alter the outcome of the larger statement. In this question you are tasked with showing that associativity holds on multiplication for at least one example. You must represent this example visually (using number lines) and algebraically. (You must use three numbers unique from one another and all of them must have an absolute value larger than 1)
The Commutative Property is obtained by an operator when the order of the two input instances does not alter the outcome. In this question you are tasked with showing that commutativity holds on multiplication for at least one example. You must represent this example visually (using number lines) and algebraically. (You must use two numbers unique from one another and both of them must have an absolute value larger than 2)
The Associative Property is attained by many operators, but not all. In this question you are tasked with showing that associativity does NOT hold on subtraction for at least one example. You must represent this example visually (using number lines) and algebraically. (You must use three numbers unique from one another and all of them must have an absolute value larger than 3)
The Commutative Property is attained by many operators, but not all. Just as before, in this question you are tasked with showing that commutativity does NOT hold on subtraction for at least one example. You must represent this example visually (using number lines) and algebraically. (You must use two numbers unique from one another and both of them must have an absolute value larger than 2)
We saw in class that the Identity property was obtained when there was a special instance within a type for an operator, such that when the operator was used, the non-special input instance remained unchanged. For Subtraction and Multiplication, give the special instances that prove Subtraction and Multiplication have this property.
Our previous investigation led us naturally to do the same for Division, but we saw that when only using Integers, the Closure property was not obtained! This led us to build a version of division that did obtain closure within the Integers.
While Integer division worked, it was unsatisfying that it left the vast majority of Integers "out in the cold". Thus we needed a way to speak about the areas left behind. This gave us Modulus!
Modulus and Integer division, as a pair, gave us the ability to fully describe the integers during factorization, and in the following section we will perform some practice with the operators!
In class we saw that integer division by 3 caused the entire number line to turn into just the multiples/factors of 3. However, losing 66% of the Integers was not ideal, so Modulo picked up the slack. The integers modulo 3 turned our inputs into "hops" or increments along a ring of length 3. However, what happens if we increment Modulo on the same number?
Not very exciting it seems. However, what if we decrement?
Modulo 2, 1, and 0 actually raise some valuable questions regarding number theory. In the following sub-problems, investigate modulo's relationship to larger concepts in the Integers.
Evaluate the following:
Briefly explain why modulo 2 seems to test for even-ness/odd-ness!
Evaluate the following:
Briefly explain why modulo 1 seems to map everything to 0!
Evaluate the following:
Briefly explain your findings!
With all those problems completed we now say good-bye to the Numbers standard. We covered topics from Number Theory and Abstract Algebra through the lens of Type Theory.
We will use this knowledge of the Booleans, Integers, and their operators as a base to investigate and explore new Types and new operators for Grouping and Ordering our instances!
In this programming assignment you will apply your understanding of type theory and operations to build a farm management system in Python!
Your repository will contain the following files:
CMSI-2820-HW2/
├── .gitignore
├── farm.py
├── test_farm.py
└── README.md
As a refresher, here is the helper video that goes from complete start to finish for the process of receiving, setting up, and turning in your programming portion of the HW:
The creative endeavor I am suggesting for Logic is to apply your logic knowledge to a real world event/experience/memory! (However always remember that you can work out an alternate creative endeavour if you want to involve your hobbies! You can make creative works in any form such as games, drawings, paintings, dioramas, sculptures, videos, fake blogs, memes, anything!) (For instance, while I am working on this HW I am listening to music! Want to analyze a song with logic? Write your own logical song? Go for it!) (Just make sure to talk to me first!)
We saw in class that Logic, while being a greater philosophical topic, is about evaluation of truth and the inference of new truths! I would like you to take any "playground" argument and convince me of your beliefs about it!
Any argument with no stakes in harming others, such as:
You are allowed to make your own "playground" argument if you'd like.
Take your playground argument and use the tools we saw in class to prove to me your stance on the matter is correct:
You don't need to use all the tools we saw in class to make a good argument to me, however, the more tools you do use, the more points you get!
This optional project can be submitted until one week after the homework due date.
| Component | Points | Description |
|---|---|---|
| Q1 | 6 | Type notation practice |
| Q2 | 14 | Constructive proofs and type evaluation |
| Q3-Q5 | 12 | Boolean algebra laws |
| Q6-Q10 | 10 | Properties of operators |
| Q11-Q13 | 18 | Modular arithmetic |
| Programming | 40 | Farm management system in Python |
| Optional Section | 20 | Logic creative project (Points For S1 Only) |
| Total | 100 |