They are in a Fitch system, using the vertical bar | to indent subproofs. Every line needs a justification written, and we distinguish between premises and temporary assumptions by “Premise” and “Assume”. For example:

Hi Ian, this is helpful, but is this example you’ve posted exactly what formal proofs look like for students? As you know, in pen-and-paper Fitch systems students can distinguish between nested assumptions and their parent temporary assumptions. I’m worried that if things look exactly as you’ve displayed, this important element is missing.

Hi Peter–thanks for asking. I’ll attach an image here of an example with nested subproofs. This is an interactive content from ch. 15, so it’s exactly what students see and work with.

Basically, nested subproofs get multiple indentations like this:

13. | | ~((P->Q)->(P->R))

As you can see in the attachment, in many textbook activities the subproof structure is given. But sometimes the book makes them type the subproof bars.

I like giving a structure in complex problems because one can scaffold learning really well. It becomes like a Sudoku puzzle, when given numbers are like a constraint. But in my class time I also emphasize a lot of free form/experimental proof writing.

Even when the structure is given and students fill in the banks, this system does not automatically tell them when one subproofs ends and another begins, when the proofs are of the same level (like the proof by cases example I gave above). So they have to figure out which line to write “Assume” on to end the first subproof and start the second.

If you want to check out all the specifics in the book, just let me know and I’ll get you a copy of the book!

Yes, exactly. Students can complete the whole textbook with just a phone if they have limited access to wifi, and they can use a phone or tablet if they don’t have a computer. We’ve created a simple system, like # for the contradiction symbol, -> for conditional, A and E for the quantifiers. Our system is also much more readable than others I’ve seen online. For example, we use v for disjunction. See how readable this is: ~P&(QvR). The interactive textbook also constantly trains students to write and read formulas made up of just keyboard characters, so it is very intuitive for them.

What do formal proofs look like?

They are in a Fitch system, using the vertical bar | to indent subproofs. Every line needs a justification written, and we distinguish between premises and temporary assumptions by “Premise” and “Assume”. For example:

Hi Ian, this is helpful, but is this example you’ve posted exactly what formal proofs look like for students? As you know, in pen-and-paper Fitch systems students can distinguish between nested assumptions and their parent temporary assumptions. I’m worried that if things look exactly as you’ve displayed, this important element is missing.

Hi Peter–thanks for asking. I’ll attach an image here of an example with nested subproofs. This is an interactive content from ch. 15, so it’s exactly what students see and work with.

Basically, nested subproofs get multiple indentations like this:

13. | | ~((P->Q)->(P->R))

As you can see in the attachment, in many textbook activities the subproof structure is given. But sometimes the book makes them type the subproof bars.

I like giving a structure in complex problems because one can scaffold learning really well. It becomes like a Sudoku puzzle, when given numbers are like a constraint. But in my class time I also emphasize a lot of free form/experimental proof writing.

Even when the structure is given and students fill in the banks, this system does not automatically tell them when one subproofs ends and another begins, when the proofs are of the same level (like the proof by cases example I gave above). So they have to figure out which line to write “Assume” on to end the first subproof and start the second.

If you want to check out all the specifics in the book, just let me know and I’ll get you a copy of the book!

Ian, just sent you an email at your UW email!

Can students type all the symbols in the system from a standard keyboard? How do you handle special symbols or characters?

Yes, exactly. Students can complete the whole textbook with just a phone if they have limited access to wifi, and they can use a phone or tablet if they don’t have a computer. We’ve created a simple system, like # for the contradiction symbol, -> for conditional, A and E for the quantifiers. Our system is also much more readable than others I’ve seen online. For example, we use v for disjunction. See how readable this is: ~P&(QvR). The interactive textbook also constantly trains students to write and read formulas made up of just keyboard characters, so it is very intuitive for them.