# zoxiy user guide

--- by s.butterfill@warwick.ac.uk

Some notes on using zoxiy to complete logic exercises (writing proofs, creating counterexamples, ...).

## Start here:

### zoxiy

There are logic exercises associated with each lecture. This is how to complete them ...

## For students:

### Symbols and Words

proof ex-proof ex-trans

When you use zoxiy you can type words instead of using symbols. But which words stand for which symbols? Here’s a list.

### Identity

definitions ex-create

Introduces the notion of identity used in studying first-order logic. Includes example argument and the two principles. Also demonstrates how to assign names in zoxiy, and using zoxiy to make identity statements true and false.

### Contradictions, Logical Truths and Logical Possibilities

definitions ex-tt

Illustrates and defines the terms ‘contradiction’, ‘logical truth’ and ‘logical possibility’. Describes how to recognise these from truth tables. Demonstrates using zoxiy to construct truth-tables and answer questions about contradictions, logical truths and logical possibilities.

### Quantifer Rules: ∃Elim with zoxiy

proof ex-proof

Explains how to do proofs involving quantifier rules with zoxiy. (Where you need to put the name ‘a’ in a box, write ‘[a]’.)

### zoxiy: Creating Possible Situations

ex-create

Describes how to create possible situations in logic-ex.

### Formal Counterexamples with zoxiy

counterexamples ex-counter

### Counterexamples

definitions ex-create

Explains the notion of a counterexample. Discusses a counterexample to a simple argument. Demonstrates using zoxiy to construct a counterexample involving shape and size properties.

### Formal Proof: ∧Elim and ∧Intro

proof ex-proof

Introduces and illustrates the use of rules of proof for conjunction. Explains how to create proofs using logic-ex.

### Subproofs with zoxiy

proof proof-example ex-proof

Introduction to the rules of proof for →, →Intro and →Elim. This is the first time subproofs are used. Also illustrates a proof without any premises. The proof is from premises P→Q and Q→R to conclusion P→R.

### Zoxiy world predicates ex-create

Defines the predicates such as ‘Happy(x)’ and ‘Crying(x)’ used in creating possible worlds.

### Creating possible situations ex-create

A quick guide to creating possible situations in zoxiy.

## For tutors:

### Monitoring Students’ Progress

tutors

How to check what students’ have completed, whether they are getting the answers right and what their answers are.