How do I display verification of propositional logic in this way?

You can type in the truth table with a rather natural syntax, provided some work behind the scenes is done.

\documentclass{article}
\usepackage{xparse,array}

\ExplSyntaxOn
\NewDocumentCommand{\truthtable}{mm}
 {
  \group_begin:
  \setlength{\arraycolsep}{0pt}
  \crocket_truth_make_preamble:n { #1 }
  \crocket_truth_make_body:n { #2 }
  \crocket_truth_make:
  \group_end:
 }

% variables
\tl_new:N \l__crocket_truth_preamble_tl
\tl_new:N \l__crocket_truth_first_tl
\tl_new:N \l__crocket_truth_body_tl
\seq_new:N \l__crocket_truth_rows_seq

% internal functions
\cs_new_protected:Nn \crocket_truth_make_preamble:n
 {
  \tl_clear:N \l__crocket_truth_preamble_tl
  \tl_clear:N \l__crocket_truth_first_tl
  % examine the first argument in order to build the table
  % preamble and the first row
  \tl_map_inline:nn { #1 }
   {
    \tl_if_in:VnTF \c_crocket_truth_delims_tl { ##1 }
     {% a delimiter is inserted in @{...} as a phantom (almost)
      % and not taken into account for the first row
      \tl_put_right:Nn \l__crocket_truth_preamble_tl { @{ \__crocket_truth_delim:n {##1} } }
     }
     {
      \tl_if_eq:nnTF { | } { ##1 }
       {% vertical bar is ignored in the rows, but it gives a | in
        % the table preamble (actually, quad | quad)
        \tl_put_right:Nn \l__crocket_truth_preamble_tl { @{\hspace{1em}}|@{\hspace{1em}} }
       }
       {% otherwise, c is added to the table preamble and
        % the item to the first row
        \tl_put_right:Nn \l__crocket_truth_preamble_tl { c }
        \tl_put_right:Nn \l__crocket_truth_first_tl { ##1 & }
       }
     }
   }
  % since rows will end with &, we add a dummy trailing column
  \tl_put_right:Nn \l__crocket_truth_preamble_tl { c } % empty last column
 }

\cs_new_protected:Nn \crocket_truth_make_body:n
 {% start building the table body
  \tl_clear:N \l__crocket_truth_body_tl
  % split the argument at \\
  \seq_set_split:Nnn \l__crocket_truth_rows_seq { \\ } { #1 }
  % and map it
  \seq_map_inline:Nn \l__crocket_truth_rows_seq
   {% each item is a row; map it to add &
    \tl_map_inline:nn { ##1 }
     {% but ignoring |
      \tl_if_eq:nnF { | } { ####1 }
       {
        \tl_put_right:Nn \l__crocket_truth_body_tl { \crocket_truth_tf:n { ####1 } & }
       }
     }
    % append the row terminator
    \tl_put_right:Nn \l__crocket_truth_body_tl { \\ }
   }
 }

\cs_new_protected:Nn \crocket_truth_make:
 {% make the table
  \exp_args:NnV \begin {array} \l__crocket_truth_preamble_tl
  % temporary define \__crocket_truth_delim:n to produce its argument
  \noalign { \cs_gset_eq:NN \__crocket_truth_delim:n \use:n }
  % output the first row
  \tl_use:N \l__crocket_truth_first_tl \\
  \hline
  % make \__crocket_truth_delim:n to deliver a phantom
  \noalign { \cs_gset_eq:NN \__crocket_truth_delim:n \hphantom }
  \tl_use:N \l__crocket_truth_body_tl
  \end{array}
 }

\cs_new_protected:Nn \crocket_truth_tf:n { \makebox[1.2em]{ $ \mathrm { #1 }$ } }

\tl_const:Nn \c_crocket_truth_delims_tl { ()[]\{\} }

\ExplSyntaxOff



\begin{document}

\[
\truthtable{
  P Q | (P \land Q)\lor P
}{
  T T | T T T T T\\
  T F | T F F T T
}
\]

\[
\truthtable{
  P Q R S | (\{ S \land \lnot ( Q \land \lnot P )\} \lor \{ R \lor \lnot \lnot Q \})
}{
  T F F F | F F T F F F T F F F F T F\\
  T F F F | F F T F F F T F F F F T F\\
  T F F F | F F T F F F T F F F F T F\\
  T F F F | F F T F F F T F F F F T F
}
\]
\end{document}

Logic is not all that well supported in LaTeX, unfortunately. At least, if it is, I haven't managed to track down the support. Everything always seems to involve a solution intended for some other problem and making it do something else.

If you have the patience, you could use something like this. I find tabular less hassle than a maths environment because all the Ts and Fs and Ps and Qs and so on need to be in what is essentially a text font anyway. (At least if your text font is also used for operators and so on in maths mode, which is usual.) And switching into maths mode for other things is less of a pain than typing \text{} all the time for text mode.

\documentclass[oneside,12pt]{article}
\usepackage{microtype}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{amsmath}
\begin{document}
  \begin{tabular}{*{4}{c}|r@{}ccc@{\thinspace}r@{}*{3}{c}@{\thinspace}c@{}lcr@{}*{3}{c}@{\thinspace}c@{\thinspace}c@{}l}
  P&Q&R&S&$(\{$&S&$\land$&$\lnot$&$($&Q &$\land$& $\lnot$&P&$)\}$&$\lor$&$\{$&R&$\lor$&$\lnot$&$\lnot$&Q&$\})$\\\hline
  T&F&F&F& &F&F&T&& F&F&F&T &&F &&F&F&F&T&F\\
\end{tabular}
\end{document}

There are scripts which will produce the tables for you, but if you are learning logic, that's no good because you need to figure out the tables for yourself. If you are teaching logic, on the other hand, they can be very useful. They don't do the spacing adjustments I included here, either. At least, the one I used didn't.