Theoretical computer science - Venn diagrams

Welcome at web application for teaching of how to use Venn diagrams on determination if in limited predicate logic a conclusion logically follows from an assumptions.
This application has been developed as a part of bachelor's thesis.

Logical operations

A logical operation is a type of operation whose input arguments are truthful values, either logical 1 - true or logical 0 - false. The output of a logical operation is also truthful value of 1 or 0, which depends on the inputs of the specific operation. Such operations are represented in predicate logic by logical conjunctions, where the most commonly used include ¬ - negation, ∧ - conjunction, ∨ - disjunction, → - implications and ↔ - equivalence.
A B ¬A A∧B A∨B A→B A↔B
1 1 0 1 1 1 1
1 0 0 0 1 0 0
0 1 1 0 1 1 0
0 0 1 0 0 1 1

Predicate logic

Follows most important extract of presentations (doc. Ing. Zdeněk Sawa, Ph.D.) of UTI subject.
  • Universe - A universe can be any non-empty set of objects. Objects from this universe are called elements of the universe. There are no universe elements in the application.
  • Variables - Individual variables represent the properties of predicates, which can take on arbitrary values from the universe. The variables are then divided into free and bound variables. Free variables occur in a formula without a quantifier. Variables are marked with a lowercase letter.
  • Constants - If the unary predicate N satisfies exactly one element x from the universe (only for this element is the valid formula N(x)), it may be useful to name this element and avoid the N predicate. In atomic formulas, constants may occur in the same places as variables, but they must not be quantified across constants. Constants are also marked with a lowercase letter.
  • Functions - The functions are not used, when displaying predicate logic formulas in Venn diagrams.
  • Terms - If x is a variable, then x is a well-formed term. If c is a constant symbol, then c is a well-formed term.
  • Predicates - Predicates represent elementary formulas of predicate logic. They can represent qualities and relationships. We interpret predicates as relations. Their arguments are terms.
  • Quantifiers - we have two types, the first: universal - mostly written as ∀, can be translated into natural language as "for all, elements from the universe" second: existential - mostly written as ∃, we translate into natural language as "there is an element".
  • Definition of predicate logic's formulas
    • If P is a predicate symbol with arity n and t1, t2, ..., tn are well-formed terms, then P (t1, t2, ..., tn) is a well-formed atomic formula.
    • Well-formed atomic formulas are well-formed formulas.
    • If φ and ψ are well-formed formulas, then also (¬φ), (φ ∧ ψ), (φ ∨ ψ), (φ → ψ) and, (φ ↔ ψ) are well-formed formulas.
    • If φ is a well-formed formula and x is a variable, then ∀xφ and ∃xφ are well-formed formula.

Limitations of predicate formulas

  • Only unary predicates are used (predicates that have only one argument).
  • There is a maximum of one quantifier in each formula and it quantifies the rest of the formula.
  • The total number of predicates in all assumptions and conclusion together is limited to a maximum of 4.
  • A maximum of one variable in any number of occurrences can occur in each formula.

Application content

The web application contains 3 main tabs:
  • Custom - on this tab you can compile your own predicate logic formulas and have the consequence evaluated from them, build syntactic trees, draw Venn diagrams, and by default hidden table of truth values.
  • Predefined - on this tab you have the only option to choose from predefined entries and the application will evaluate and display it.
  • Test - this tab offers the possibility to test the yours knowledge. After selecting the category, a random entry will be selected and you have the option interact with Venn diagram and decide if the conlusion follows from assumptions. After the check, the correctness of the answers will be evaluated.

Application control

  • Work with Inputs - when writing your own formulas, you can use several different sets of operators to choose from in the drop-down list. After clicking on the button, the selected string is written to the selected formula at the selected position, or replaces the selected text.
  • Venn diagram control - the application draws a Venn diagram with the appropriate number of sets and all the buttons that you will need to enter the prerequisites. Interaction with regions is performed as follows: the appropriate radio button is selected below the diagram and after clicking inside the region, the region is filled.
  • Test results - after clicking on the 'Check' button, the application will evaluate the correctness of the answers and display 'Expected result', 'Your answer' and possibly 'Difference' if you have misidentified any region of the Venn diagram.

Marking assumptions in the Venn diagram

  • For each assumption containing a general quantifier, we hatch the appropriate regions in which it is clear from the assumption that there is no element. For each additional assumption, the hatching is distinguished by a different degree of inclination, in the application it is inflected by repeated clicking on region.
  • A formula with an existential quantifier then speaks of the existence of elements that satisfy something. In regions where these element properties are met, we mark the symbol 'x'. If such an element could occur in more than one region, we will use the '?' symbol instead of the 'x' symbol in all those regions. By that we mean that it is not clear in which of those regions the element actually occurs. We do not mark 'x' and '?' symbols in hatched regions, because there is certainly no element in them. Application between 'x' and '?' distinguishes depending on the number of occurrences.
  • Formulas with constants, like those with an existential quantifier, speak of the existence of an element, only that element is named. In the diagram, instead of the general symbol 'x', we mark the name of the relevant constant.

Evaluation of entailment of the conclusion using the Venn diagram

A1 ¬P(b)
A2 ∃x(Z(x) ∧ P(x))
A3 ∀x(P(x) → Z(x))
C1 ∃x P(x)
C2 ∃x (¬P(x) ∧ Z(x))
C3 Z(b)
There are 3 different assumptions and 3 different conclusions on which we will explain some special scenarios that may occur.
  • C: General procedure to be followed for each conclusion:
    1. When it comes to a conclusion containing a general quantifier, the conclusion follows from the assumptions only when all regions except those specified in the conclusion formula are hatched.
    2. In the case of a conclusion containing an existential quantifier, in order for the conclusion to follow from the assumptions, at least in one of the regions of the specified conclusion formulas, at least one assumption must contain an existential quantifier or constants without the '?' symbol.
  • C1: Let's start with the first conclusion following the general procedure:
    1. The conclusion in this case follows from assumptions, because the assumption A2 speaks of the existence of an element in the set P.
  • C2:
    1. The general procedure does not talk about the possibility of finding a variable or constant with the symbol '?', in this case we need to find out if all of the connected '?' symbols are in regions specified by this conclusion.
    2. The conclusion in this case does not follow from assumptions because there is no variable or constant that would occur only in the regions specified in the conclusion.
    3. If the conclusion were ∃x¬P (x), then it would follow from assumptions, because constant b occurs only in those regions.
  • C3:
    1. In the regions specified in this conclusion, there is a variable without a question mark, but constants are a subset of variables, meaning that a variable doesn't tell us anything about whether the constant we are looking for exists in this regions or not.
    2. Therefore, the conclusion does not follow from assumptions in this case.